mathlib3

2fc49d57 - feat(group_theory/index): add 3 lemmas (#17288)