Commit 2022-04-20 17:09 7bfaa5c8

View on Github →

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.

Estimated changes

Modified src/group_theory/schreier.lean

added theorem subgroup.exists_finset_card_le_mul

added theorem subgroup.fg_of_index_ne_zero

added theorem subgroup.rank_le_index_mul_rank