mathlib3

6c48d300 - feat(group_theory/subgroup/basic): add 2 lemmas (#17987)