inverse_of_isUnit — Mathlib

English

If x is a unit in a monoid with zero, then its ring inverse equals the underlying element of its inverse unit.

Русский

Если x — единица в моноиде с нулём, то обратное x по отношению к кольцу равно элементу, лежащему в обратной единице.

LaTeX

$$$\mathrm{inverse}(x) = ((h.unit^{-1} : M_0^{\times}) : M_0)$ where $h : IsUnit(x)$$$

Lean4

theorem inverse_of_isUnit {x : M₀} (h : IsUnit x) : inverse x = ((h.unit⁻¹ : M₀ˣ) : M₀) :=
  dif_pos h

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