Additivizing subgroups?

Stream: Is there code for X?

[David Loeffler]

If G is a group, then there's obviously a bijection between subgroups of G and AddSubgroups of Additive G. Do we have code for this in mathlib?

All I found with loogle was docs#Additive.isAddSubgroup, part of the long-deprecated "un-bundled" subgroups.

[David Loeffler]

Oh wait, it's docs#Subgroup.toAddSubgroup (I hadn't thought to look in Subgroup.Lattice). Sorry for the noise.

[Floris van Doorn]

For next time: Loogle is your friend!

[Floris van Doorn]

@loogle Additive, Subgroup, Group

[loogle]

:search: AddSubgroup.toSubgroup', Subgroup.toAddSubgroup, and 10 more