mulRight_symm — Mathlib

English

The inverse of the right-multiplication order isomorphism is the right-multiplication by a^{-1}.

Русский

Обратное к правому умножению как порядковому изоморфизму является умножение на a^{-1}.

LaTeX

$$(OrderIso.mulRight(a)).symm = OrderIso.mulRight(a^{-1})$$

Lean4

@[to_additive (attr := simp)]
theorem mulRight_symm (a : α) : (OrderIso.mulRight a).symm = OrderIso.mulRight a⁻¹ :=
  by
  ext x
  rfl

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