English
There is an order isomorphism between AddSubgroup A and Subgroup (Multiplicative A), translating additive structure into multiplicative structure.
Русский
Существует упорядоченное изоморождение между AddSubgroup A и Subgroup (Multiplicative A), переводящее аддитивную структуру в мультипликативную.
LaTeX
$$$$ \\mathrm{AddSubgroup}(A) \\cong_o \\mathrm{Subgroup}(\\mathrm{Multiplicative}~A). $$$$
Lean4
/-- Additive subgroups of an additive group `A` are isomorphic to subgroups of `Multiplicative A`.
-/
@[simps!]
def toSubgroup : AddSubgroup A ≃o Subgroup (Multiplicative A)
where
toFun S := { AddSubmonoid.toSubmonoid S.toAddSubmonoid with inv_mem' := S.neg_mem' }
invFun S := { Submonoid.toAddSubmonoid S.toSubmonoid with neg_mem' := S.inv_mem' }
left_inv x := by cases x; rfl
right_inv x := by cases x; rfl
map_rel_iff' := Iff.rfl
