mathlib

6f428ed4 - feat(group_theory/schreier): Finset version of Schreier's lemma (#13274)

feat(group_theory/schreier): Finset version of Schreier's lemma (#13274) This PR adds a finset version of Schreier's lemma, getting closer to a statement in terms of `group.fg` and `group.rank`.