mathlib3 documentation

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.

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

Equations

x ↦ -x as an order-reversing equivalence.

Equations

Alias of the forward direction of inv_le'.

Alias of the forward direction of inv_le'.

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

Equations

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

Equations

Alias of the forward direction of le_inv'.

Alias of the forward direction of le_inv'.

@[simp]
@[simp]
def order_iso.div_right {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) :
α ≃o α

x ↦ x / a as an order isomorphism.

Equations
@[simp]
@[simp]
def order_iso.sub_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) :
α ≃o α

x ↦ x - a as an order isomorphism.

Equations
@[simp]
theorem order_iso.add_left_apply {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] (a x : α) :
@[simp]
theorem order_iso.mul_left_apply {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] (a x : α) :