English
There is a multiplicative equivalence between the subgroup S.ofUnits (viewed as a submonoid of M) and the subgroup S of Units M.
Русский
Существует мультипликативное эквивалентное отображение между подгруппой S.ofUnits (как подмоноидом M) и подгруппой S в единицах M.
LaTeX
$$$S^{\\mathrm{ofUnits}} \\cong_* S$$$
Lean4
/-- The equivalence between the coercion of a subgroup `S` of `Mˣ` to a submonoid of `M` and
the subgroup itself as a type. -/
@[to_additive /-- The equivalence between the coercion of an additive subgroup `S` of
`Mˣ` to an additive submonoid of `M` and the additive subgroup itself as a type. -/
]
noncomputable def ofUnitsEquivType (S : Subgroup Mˣ) : S.ofUnits ≃* S
where
toFun := fun x => ⟨S.unit_of_mem_ofUnits x.2, S.unit_of_mem_ofUnits_spec_mem⟩
invFun := fun x => ⟨x.1, ⟨x.1, x.2, rfl⟩⟩
map_mul' := fun _ _ => Subtype.ext (Units.ext rfl)
