mathlib

b0991037 - feat(group_theory/subgroup): add `subgroup.forall_gpowers` etc (#8470)

feat(group_theory/subgroup): add `subgroup.forall_gpowers` etc (#8470) * add `subgroup.forall_gpowers`, `subgroup.exists_gpowers`, `subgroup.forall_mem_gpowers`, and `subgroup.exists_mem_gpowers`; * add their additive counterparts; * drop some explicit lemmas about `add_subgroup.gmultiples`: `to_additive` can generate them now.