Inverse and multiplication as order isomorphisms in ordered groups #
x ↦ x⁻¹
as an order-reversing equivalence.
Equations
Instances For
x ↦ -x
as an order-reversing equivalence.
Equations
Instances For
@[simp]
theorem
OrderIso.neg_symm_apply
(α : Type u)
[AddGroup α]
[LE α]
[AddLeftMono α]
[AddRightMono α]
(a✝ : αᵒᵈ)
:
@[simp]
theorem
OrderIso.inv_apply
(α : Type u)
[Group α]
[LE α]
[MulLeftMono α]
[MulRightMono α]
(a✝ : α)
:
@[simp]
theorem
OrderIso.inv_symm_apply
(α : Type u)
[Group α]
[LE α]
[MulLeftMono α]
[MulRightMono α]
(a✝ : αᵒᵈ)
:
@[simp]
theorem
OrderIso.neg_apply
(α : Type u)
[AddGroup α]
[LE α]
[AddLeftMono α]
[AddRightMono α]
(a✝ : α)
:
theorem
inv_le_of_inv_le'
{α : Type u}
[Group α]
[LE α]
[MulLeftMono α]
[MulRightMono α]
{a b : α}
:
Alias of the forward direction of inv_le'
.
theorem
neg_le_of_neg_le
{α : Type u}
[AddGroup α]
[LE α]
[AddLeftMono α]
[AddRightMono α]
{a b : α}
:
x ↦ a / x
as an order-reversing equivalence.
Equations
Instances For
x ↦ a - x
as an order-reversing equivalence.
Equations
Instances For
@[simp]
theorem
OrderIso.divLeft_apply
{α : Type u}
[Group α]
[LE α]
[MulLeftMono α]
[MulRightMono α]
(a a✝ : α)
:
@[simp]
theorem
OrderIso.subLeft_apply
{α : Type u}
[AddGroup α]
[LE α]
[AddLeftMono α]
[AddRightMono α]
(a a✝ : α)
:
@[simp]
theorem
OrderIso.subLeft_symm_apply
{α : Type u}
[AddGroup α]
[LE α]
[AddLeftMono α]
[AddRightMono α]
(a : α)
(a✝ : αᵒᵈ)
:
@[simp]
theorem
OrderIso.divLeft_symm_apply
{α : Type u}
[Group α]
[LE α]
[MulLeftMono α]
[MulRightMono α]
(a : α)
(a✝ : αᵒᵈ)
:
Alias of the forward direction of le_inv'
.
theorem
le_neg_of_le_neg
{α : Type u}
[AddGroup α]
[LE α]
[AddLeftMono α]
[AddRightMono α]
{a b : α}
:
@[simp]
@[simp]
@[simp]
@[simp]
x ↦ x / a
as an order isomorphism.
Equations
Instances For
x ↦ x - a
as an order isomorphism.
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]