Commit 2021-10-08 10:04 34145b7f
View on Github →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?)