mathlib3

28c902d8 - fix(algebra/group/pi): Fix apply-simp-lemmas for monoid_hom.single (#12474)

fix(algebra/group/pi): Fix apply-simp-lemmas for monoid_hom.single (#12474) so that the simp-normal form really is `pi.mul_single`. While adjusting related lemmas in `group_theory.subgroup.basic`, add a few missing `to_additive` attributes.