# mathlib3documentation

algebra.order.group.order_iso

# 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 α] (ᾰ : α) :
=
@[simp]
theorem order_iso.neg_symm_apply (α : Type u) [add_group α] [has_le α] (ᾰ : αᵒᵈ) :
def order_iso.inv (α : Type u) [group α] [has_le α]  :

x ↦ x⁻¹ as an order-reversing equivalence.

Equations
@[simp]
theorem order_iso.inv_apply (α : Type u) [group α] [has_le α] (ᾰ : α) :
def order_iso.neg (α : Type u) [add_group α] [has_le α]  :

x ↦ -x as an order-reversing equivalence.

Equations
@[simp]
theorem order_iso.inv_symm_apply (α : Type u) [group α] [has_le α] (ᾰ : αᵒᵈ) :
=
theorem neg_le {α : Type u} [add_group α] [has_le α] {a b : α} :
-a b -b a
theorem inv_le' {α : Type u} [group α] [has_le α] {a b : α} :
theorem inv_le_of_inv_le' {α : Type u} [group α] [has_le α] {a b : α} :

Alias of the forward direction of inv_le'.

theorem neg_le_of_neg_le {α : Type u} [add_group α] [has_le α] {a b : α} :
-a b -b a

Alias of the forward direction of inv_le'.

theorem le_neg {α : Type u} [add_group α] [has_le α] {a b : α} :
a -b b -a
theorem le_inv' {α : Type u} [group α] [has_le α] {a b : α} :
@[simp]
theorem order_iso.sub_left_symm_apply {α : Type u} [add_group α] [has_le α] (a : α) (ᾰ : αᵒᵈ) :
=
@[simp]
theorem order_iso.div_left_symm_apply {α : Type u} [group α] [has_le α] (a : α) (ᾰ : αᵒᵈ) :
=
@[simp]
theorem order_iso.sub_left_apply {α : Type u} [add_group α] [has_le α] (a ᾰ : α) :
def order_iso.div_left {α : Type u} [group α] [has_le α] (a : α) :

x ↦ a / x as an order-reversing equivalence.

Equations
@[simp]
theorem order_iso.div_left_apply {α : Type u} [group α] [has_le α] (a ᾰ : α) :
def order_iso.sub_left {α : Type u} [add_group α] [has_le α] (a : α) :

x ↦ a - x as an order-reversing equivalence.

Equations
theorem le_inv_of_le_inv {α : Type u} [group α] [has_le α] {a b : α} :

Alias of the forward direction of le_inv'.

theorem le_neg_of_le_neg {α : Type u} [add_group α] [has_le α] {a b : α} :
a -b b -a

Alias of the forward direction of le_inv'.

@[simp]
theorem order_iso.add_right_apply {α : Type u} [add_group α] [has_le α] (a x : α) :
x = x + a
@[simp]
theorem order_iso.mul_right_apply {α : Type u} [group α] [has_le α] (a x : α) :
x = x * a
@[simp]
theorem order_iso.mul_right_to_equiv {α : Type u} [group α] [has_le α] (a : α) :
def order_iso.add_right {α : Type u} [add_group α] [has_le α] (a : α) :
α ≃o α

equiv.add_right as an order_iso. See also order_embedding.add_right.

Equations
def order_iso.mul_right {α : Type u} [group α] [has_le α] (a : α) :
α ≃o α

equiv.mul_right as an order_iso. See also order_embedding.mul_right.

Equations
@[simp]
theorem order_iso.add_right_to_equiv {α : Type u} [add_group α] [has_le α] (a : α) :
@[simp]
theorem order_iso.add_right_symm {α : Type u} [add_group α] [has_le α] (a : α) :
@[simp]
theorem order_iso.mul_right_symm {α : Type u} [group α] [has_le α] (a : α) :
@[simp]
theorem order_iso.div_right_symm_apply {α : Type u} [group α] [has_le α] (a b : α) :
b = b * a
@[simp]
theorem order_iso.sub_right_symm_apply {α : Type u} [add_group α] [has_le α] (a b : α) :
b = b + a
def order_iso.div_right {α : Type u} [group α] [has_le α] (a : α) :
α ≃o α

x ↦ x / a as an order isomorphism.

Equations
@[simp]
theorem order_iso.sub_right_apply {α : Type u} [add_group α] [has_le α] (a b : α) :
b = b - a
@[simp]
theorem order_iso.div_right_apply {α : Type u} [group α] [has_le α] (a b : α) :
b = b / a
def order_iso.sub_right {α : Type u} [add_group α] [has_le α] (a : α) :
α ≃o α

x ↦ x - a as an order isomorphism.

Equations
@[simp]
theorem order_iso.mul_left_to_equiv {α : Type u} [group α] [has_le α] (a : α) :
@[simp]
theorem order_iso.add_left_to_equiv {α : Type u} [add_group α] [has_le α] (a : α) :
@[simp]
theorem order_iso.add_left_apply {α : Type u} [add_group α] [has_le α] (a x : α) :
x = a + x
def order_iso.add_left {α : Type u} [add_group α] [has_le α] (a : α) :
α ≃o α

equiv.add_left as an order_iso. See also order_embedding.add_left.

Equations
@[simp]
theorem order_iso.mul_left_apply {α : Type u} [group α] [has_le α] (a x : α) :
x = a * x
def order_iso.mul_left {α : Type u} [group α] [has_le α] (a : α) :
α ≃o α

equiv.mul_left as an order_iso. See also order_embedding.mul_left.

Equations
@[simp]
theorem order_iso.mul_left_symm {α : Type u} [group α] [has_le α] (a : α) :
@[simp]
theorem order_iso.add_left_symm {α : Type u} [add_group α] [has_le α] (a : α) :