Inverse and multiplication as order isomorphisms in ordered groups #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[simp]
theorem
order_iso.neg_apply
(α : Type u)
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(ᾰ : α) :
⇑(order_iso.neg α) ᾰ = ⇑order_dual.to_dual (-ᾰ)
@[simp]
theorem
order_iso.neg_symm_apply
(α : Type u)
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(ᾰ : αᵒᵈ) :
⇑(rel_iso.symm (order_iso.neg α)) ᾰ = -⇑order_dual.of_dual ᾰ
def
order_iso.inv
(α : Type u)
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le] :
x ↦ x⁻¹ as an order-reversing equivalence.
Equations
- order_iso.inv α = {to_equiv := equiv.trans (equiv.inv α) order_dual.to_dual, map_rel_iff' := _}
@[simp]
theorem
order_iso.inv_apply
(α : Type u)
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(ᾰ : α) :
⇑(order_iso.inv α) ᾰ = ⇑order_dual.to_dual ᾰ⁻¹
def
order_iso.neg
(α : Type u)
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le] :
x ↦ -x as an order-reversing equivalence.
Equations
- order_iso.neg α = {to_equiv := equiv.trans (equiv.neg α) order_dual.to_dual, map_rel_iff' := _}
@[simp]
theorem
order_iso.inv_symm_apply
(α : Type u)
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(ᾰ : αᵒᵈ) :
⇑(rel_iso.symm (order_iso.inv α)) ᾰ = (⇑order_dual.of_dual ᾰ)⁻¹
theorem
neg_le
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α} :
theorem
inv_le'
{α : Type u}
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α} :
theorem
inv_le_of_inv_le'
{α : Type u}
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α} :
Alias of the forward direction of inv_le'.
theorem
neg_le_of_neg_le
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α} :
Alias of the forward direction of inv_le'.
theorem
le_neg
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α} :
theorem
le_inv'
{α : Type u}
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α} :
theorem
le_inv_of_le_inv
{α : Type u}
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α} :
Alias of the forward direction of le_inv'.
theorem
le_neg_of_le_neg
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α} :
Alias of the forward direction of le_inv'.
@[simp]
theorem
order_iso.add_right_apply
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(a x : α) :
⇑(order_iso.add_right a) x = x + a
@[simp]
theorem
order_iso.mul_right_apply
{α : Type u}
[group α]
[has_le α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(a x : α) :
⇑(order_iso.mul_right a) x = x * a
@[simp]
theorem
order_iso.mul_right_to_equiv
{α : Type u}
[group α]
[has_le α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(a : α) :
def
order_iso.add_right
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(a : α) :
α ≃o α
equiv.add_right as an order_iso. See also order_embedding.add_right.
Equations
- order_iso.add_right a = {to_equiv := equiv.add_right a, map_rel_iff' := _}
def
order_iso.mul_right
{α : Type u}
[group α]
[has_le α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(a : α) :
α ≃o α
equiv.mul_right as an order_iso. See also order_embedding.mul_right.
Equations
- order_iso.mul_right a = {to_equiv := equiv.mul_right a, map_rel_iff' := _}
@[simp]
theorem
order_iso.add_right_to_equiv
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(a : α) :
@[simp]
theorem
order_iso.add_right_symm
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(a : α) :
(order_iso.add_right a).symm = order_iso.add_right (-a)
@[simp]
theorem
order_iso.mul_right_symm
{α : Type u}
[group α]
[has_le α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(a : α) :
@[simp]
theorem
order_iso.mul_left_to_equiv
{α : Type u}
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
(a : α) :
@[simp]
theorem
order_iso.add_left_to_equiv
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
(a : α) :
@[simp]
theorem
order_iso.add_left_apply
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
(a x : α) :
⇑(order_iso.add_left a) x = a + x
def
order_iso.add_left
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
(a : α) :
α ≃o α
equiv.add_left as an order_iso. See also order_embedding.add_left.
Equations
- order_iso.add_left a = {to_equiv := equiv.add_left a, map_rel_iff' := _}
@[simp]
theorem
order_iso.mul_left_apply
{α : Type u}
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
(a x : α) :
⇑(order_iso.mul_left a) x = a * x
def
order_iso.mul_left
{α : Type u}
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
(a : α) :
α ≃o α
equiv.mul_left as an order_iso. See also order_embedding.mul_left.
Equations
- order_iso.mul_left a = {to_equiv := equiv.mul_left a, map_rel_iff' := _}
@[simp]
theorem
order_iso.mul_left_symm
{α : Type u}
[group α]
[has_le α]
[covariant_class α α has_mul.mul has_le.le]
(a : α) :
@[simp]
theorem
order_iso.add_left_symm
{α : Type u}
[add_group α]
[has_le α]
[covariant_class α α has_add.add has_le.le]
(a : α) :
(order_iso.add_left a).symm = order_iso.add_left (-a)