English
There is a natural order isomorphism between the lattice of subgroups of G and the lattice of additive subgroups of the additive group Additive G.
Русский
Существует естественное упорядоченное изоморфизм между решёткой подгрупп G и решёткой аддитивных подгрупп добавочного группы Additive G.
LaTeX
$$$$ \mathrm{Subgroup}(G) \\cong_o \\mathrm{AddSubgroup}(\\mathrm{Additive}~G). $$$$
Lean4
/-- Subgroups of a group `G` are isomorphic to additive subgroups of `Additive G`. -/
@[simps!]
def toAddSubgroup : Subgroup G ≃o AddSubgroup (Additive G)
where
toFun S := { Submonoid.toAddSubmonoid S.toSubmonoid with neg_mem' := S.inv_mem' }
invFun S := { AddSubmonoid.toSubmonoid S.toAddSubmonoid with inv_mem' := S.neg_mem' }
left_inv x := by cases x; rfl
right_inv x := by cases x; rfl
map_rel_iff' := Iff.rfl
