divRight₀ — Mathlib

English

The divRight₀ construction provides an order isomorphism for positive elements.

Русский

Конструкция divRight₀ образует изоморфизм порядка для положительных элементов.

LaTeX

$$OrderIso.divRight₀(\cdot)$$

Lean4

/-- `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_iff_left₀ (a := a⁻¹) (Right.inv_pos.mpr ha)

Похожие утверждения