mathlib
7bfaa5c8 - feat(group_theory/schreier): Schreier's lemma in terms of `group.fg` and `group.rank` (#13361)

Commit

3 years ago

feat(group_theory/schreier): Schreier's lemma in terms of `group.fg` and `group.rank` (#13361) This PR adds statements of Schreier's lemma in terms of `group.fg` and `group.rank`.

Author

tb65536

Parents

b0805a5e

mathlib 7bfaa5c8 - feat(group_theory/schreier): Schreier's lemma in terms of `group.fg` and `group.rank` (#13361)

mathlib
7bfaa5c8 - feat(group_theory/schreier): Schreier's lemma in terms of `group.fg` and `group.rank` (#13361)