ofUnits_right_inverse — Mathlib

English

There is a right inverse: composing Submonoid.units with ofUnits yields the identity on Submonoid M.

Русский

Существуют правые противобразования: применяя Submonoid.units затем ofUnits даёт исходное подмоноид.

LaTeX

$$$\\forall S \\in Submonoid(M),\\; \\mathrm{ofUnits}(\\mathrm{Submonoid.units}(S)) = S$$$

Lean4

@[to_additive]
theorem ofUnits_right_inverse : Function.RightInverse (ofUnits (M := M)) (Submonoid.units (M := M)) :=
  ofUnits_units_gci.u_l_leftInverse

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