# Inverse and multiplication as order isomorphisms in ordered groups #

def OrderIso.neg (α : Type u) [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :

x ↦ -x as an order-reversing equivalence.

Equations
Instances For
@[simp]
theorem OrderIso.inv_apply (α : Type u) [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] :
∀ (a : α), (OrderIso.inv α) a = OrderDual.toDual a⁻¹
@[simp]
theorem OrderIso.neg_apply (α : Type u) [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
∀ (a : α), (OrderIso.neg α) a = OrderDual.toDual (-a)
@[simp]
theorem OrderIso.neg_symm_apply (α : Type u) [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
∀ (a : αᵒᵈ), (RelIso.symm (OrderIso.neg α)) a = -OrderDual.ofDual a
@[simp]
theorem OrderIso.inv_symm_apply (α : Type u) [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] :
∀ (a : αᵒᵈ), (RelIso.symm (OrderIso.inv α)) a = (OrderDual.ofDual a)⁻¹
def OrderIso.inv (α : Type u) [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] :

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

Equations
Instances For
theorem neg_le {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} :
-a b -b a
theorem inv_le' {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} :
theorem inv_le_of_inv_le' {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} :
a⁻¹ bb⁻¹ a

Alias of the forward direction of inv_le'.

theorem neg_le_of_neg_le {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} :
-a b-b a
theorem le_neg {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} :
a -b b -a
theorem le_inv' {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} :
def OrderIso.subLeft {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :

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

Equations
• = { toEquiv := .trans OrderDual.toDual, map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.divLeft_apply {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
∀ (a_1 : α), a_1 = OrderDual.toDual (a / a_1)
@[simp]
theorem OrderIso.subLeft_symm_apply {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
∀ (a_1 : αᵒᵈ), a_1 = -OrderDual.ofDual a_1 + a
@[simp]
theorem OrderIso.divLeft_symm_apply {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
∀ (a_1 : αᵒᵈ), a_1 = (OrderDual.ofDual a_1)⁻¹ * a
@[simp]
theorem OrderIso.subLeft_apply {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
∀ (a_1 : α), a_1 = OrderDual.toDual (a - a_1)
def OrderIso.divLeft {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :

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

Equations
• = { toEquiv := .trans OrderDual.toDual, map_rel_iff' := }
Instances For
theorem le_inv_of_le_inv {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} :
a b⁻¹b a⁻¹

Alias of the forward direction of le_inv'.

theorem le_neg_of_le_neg {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} :
a -bb -a
def OrderIso.addRight {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
α ≃o α

Equiv.addRight as an OrderIso. See also OrderEmbedding.addRight.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
theorem OrderIso.addRight.proof_1 {α : Type u_1} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
∀ {x x_1 : α}, x + a x_1 + a x x_1
@[simp]
theorem OrderIso.mulRight_apply {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (x : α) :
x = x * a
@[simp]
theorem OrderIso.mulRight_toEquiv {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
.toEquiv =
@[simp]
theorem OrderIso.addRight_apply {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (x : α) :
x = x + a
@[simp]
theorem OrderIso.addRight_toEquiv {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
.toEquiv =
def OrderIso.mulRight {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
α ≃o α

Equiv.mulRight as an OrderIso. See also OrderEmbedding.mulRight.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.addRight_symm {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
.symm =
@[simp]
theorem OrderIso.mulRight_symm {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
.symm =
def OrderIso.subRight {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
α ≃o α

x ↦ x - a as an order isomorphism.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.divRight_apply {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
b = b / a
@[simp]
theorem OrderIso.subRight_apply {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
b = b - a
@[simp]
theorem OrderIso.divRight_symm_apply {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
b = b * a
@[simp]
theorem OrderIso.subRight_symm_apply {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (b : α) :
b = b + a
def OrderIso.divRight {α : Type u} [] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
α ≃o α

x ↦ x / a as an order isomorphism.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
def OrderIso.addLeft {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
α ≃o α

Equiv.addLeft as an OrderIso. See also OrderEmbedding.addLeft.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
theorem OrderIso.addLeft.proof_1 {α : Type u_1} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
∀ {x x_1 : α}, a + x a + x_1 x x_1
@[simp]
theorem OrderIso.addLeft_toEquiv {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
.toEquiv =
@[simp]
theorem OrderIso.mulLeft_apply {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) (x : α) :
x = a * x
@[simp]
theorem OrderIso.mulLeft_toEquiv {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
.toEquiv =
@[simp]
theorem OrderIso.addLeft_apply {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) (x : α) :
x = a + x
def OrderIso.mulLeft {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
α ≃o α

Equiv.mulLeft as an OrderIso. See also OrderEmbedding.mulLeft.

Equations
• = { toEquiv := , map_rel_iff' := }
Instances For
@[simp]
theorem OrderIso.addLeft_symm {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] (a : α) :
.symm =
@[simp]
theorem OrderIso.mulLeft_symm {α : Type u} [] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] (a : α) :
.symm =