mathlib

25d28c83 - feat(group_theory/schreier): Add version of Schreier's lemma (#13231)

feat(group_theory/schreier): Add version of Schreier's lemma (#13231) This PR adds a version of Schreier's lemma of the form `closure (_ : set H) = ⊤`, as opposed to `closure (_ : set G) = H`. This is closer to saying that `H` is finitely generated. I also fiddled with the names a bit.