Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso

OrderIso.mulLeft₀ definition

(a : G₀) (ha : 0 < a) : G₀ ≃o G₀

Full source

/-- `Equiv.mulLeft₀` as an order isomorphism. -/
@[simps! +simpRhs]
def mulLeft₀ (a : G₀) (ha : 0 < a) : G₀ ≃o G₀ where
  toEquiv := .mulLeft₀ a ha.ne'
  map_rel_iff' := mul_le_mul_left ha

Order isomorphism induced by left multiplication with a positive element

Informal description

For a group with zero $ G_0 $ and a positive element $ a \in G_0 $ (i.e., $ 0 < a $), the function $ x \mapsto a * x $ is an order isomorphism from $ G_0 $ to itself. This means it is a bijective map that preserves the order relation: for any $ x, y \in G_0 $, $ x \leq y $ if and only if $ a * x \leq a * y $.

OrderIso.mulLeft₀_symm theorem

(a : G₀) (ha : 0 < a) : (mulLeft₀ a ha).symm = mulLeft₀ a⁻¹ (inv_pos.2 ha)

Full source

lemma mulLeft₀_symm (a : G₀) (ha : 0 < a) : (mulLeft₀ a ha).symm = mulLeft₀ a⁻¹ (inv_pos.2 ha) := by
  ext; rfl

Inverse of Left Multiplication by a Positive Element as an Order Isomorphism

Informal description

For any positive element $a$ in a group with zero $G_0$ (i.e., $0 < a$), the inverse of the order isomorphism $x \mapsto a \cdot x$ is equal to the order isomorphism $x \mapsto a^{-1} \cdot x$, where $a^{-1}$ is also positive (i.e., $(a \cdot \_)^{-1} = a^{-1} \cdot \_$).

OrderIso.mulRight₀ definition

(a : G₀) (ha : 0 < a) : G₀ ≃o G₀

Full source

/-- `Equiv.mulRight₀` as an order isomorphism. -/
@[simps! +simpRhs]
def mulRight₀ (a : G₀) (ha : 0 < a) : G₀ ≃o G₀ where
  toEquiv := .mulRight₀ a ha.ne'
  map_rel_iff' := mul_le_mul_right ha

Order isomorphism induced by right multiplication with a positive element

Informal description

For a group with zero $ G_0 $ and a positive element $ a \in G_0 $ (i.e., $ 0 < a $), the function $ x \mapsto x * a $ is an order isomorphism from $ G_0 $ to itself. This means it is a bijective map that preserves the order relation: for any $ x, y \in G_0 $, $ x \leq y $ if and only if $ x * a \leq y * a $.

OrderIso.mulRight₀_symm theorem

(a : G₀) (ha : 0 < a) : (mulRight₀ a ha).symm = mulRight₀ a⁻¹ (Right.inv_pos.2 ha)

Full source

lemma mulRight₀_symm (a : G₀) (ha : 0 < a) :
    (mulRight₀ a ha).symm = mulRight₀ a⁻¹ (Right.inv_pos.2 ha) := by ext; rfl

Inverse of Right Multiplication Order Isomorphism by Positive Element

Informal description

For any element $a$ in a group with zero $G_0$ such that $0 < a$, the inverse of the order isomorphism $x \mapsto x * a$ is equal to the order isomorphism $x \mapsto x * a^{-1}$, where $a^{-1}$ is the inverse of $a$ and $0 < a^{-1}$ holds.

OrderIso.divRight₀ definition

(a : G₀) (ha : 0 < a) : G₀ ≃o G₀

Full source

/-- `Equiv.divRight₀` as an order isomorphism. -/
@[simps! +simpRhs]
def divRight₀ (a : G₀) (ha : 0 < a) : G₀ ≃o G₀ where
  toEquiv := .divRight₀ a ha.ne'
  map_rel_iff' {b c} := by
    simp only [Equiv.divRight₀_apply, div_eq_mul_inv]
    exact mul_le_mul_right (a := a⁻¹) (Right.inv_pos.mpr ha)

Order isomorphism induced by division by a positive element

Informal description

For a group with zero $ G_0 $ and a positive element $ a \in G_0 $ (i.e., $ 0 < a $), the function $ x \mapsto x / a $ is an order isomorphism from $ G_0 $ to itself. This means it is a bijective map that preserves the order relation: for any $ x, y \in G_0 $, $ x \leq y $ if and only if $ x / a \leq y / a $.