mulRight₀ — Mathlib

English

The right-multiplication isomorphism is an order isomorphism for positive elements.

Русский

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

LaTeX

$$OrderIso.mulRight₀(•, •)$$

Lean4

/-- `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_iff_left₀ ha

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