mathlib 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'.

Alias of the forward direction of le_inv'.

Alias of the forward direction of le_inv'.

@[simp]
@[simp]
@[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 : α) :