units_left_inverse — Mathlib

English

There is a left inverse relationship between the units map and the inclusion of units from Subgroup of Units.

Русский

Существуют левый обратный взаимнооднозначный отображения между единицами и включением единиц подгруппы единиц.

LaTeX

$$$ \text{LeftInverse}(\mathrm{units}, \mathrm{Subgroup.ofUnits}) $$$

Lean4

@[to_additive]
theorem units_left_inverse : Function.LeftInverse (units (M := M)) (Subgroup.ofUnits (M := M)) :=
  ofUnits_units_gci.u_l_leftInverse

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