ofUnitsTopEquiv — Mathlib

English

The top subgroup of Mˣ coerced to a submonoid is naturally isomorphic to the units of M.

Русский

Верхняя подгруппа Mˣ, приведенная к подмоноиду, естественно изоморфна единицам M.

LaTeX

$$$\\operatorname{ofUnitsTopEquiv} = (\\operatorname{ofUnitsEquivType}) \\; \\text{trans} \\; \\text{topEquiv}$$$

Lean4

/-- The equivalence between the top subgroup of `Mˣ` coerced to a submonoid `M` and the
units of `M`. -/
@[to_additive /-- The equivalence between the additive subgroup of additive units of
    `S` and the additive submonoid of additive unit elements of `S`. -/
    ]
noncomputable def ofUnitsTopEquiv : (⊤ : Subgroup Mˣ).ofUnits ≃* Mˣ :=
  (⊤ : Subgroup Mˣ).ofUnitsEquivType.trans topEquiv

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