mathlib

34145b7f - feat(group_theory/subgroup/basic): a new to_additive lemma, and remove a by hand proof (#9594)

feat(group_theory/subgroup/basic): a new to_additive lemma, and remove a by hand proof (#9594) I needed `add_subgroup.smul_mem` which didn't seem to exist, and noticed that the `add_subgroup.gsmul_mem` version is proved by hand while to_additive generates it fine (now?)