Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.exists_finset_card_le_mul

Modification history

2022-11-11 23:56
src/group_theory/schreier.lean
feat(group_theory/index): Add typeclass for `finite_index` (#17139) …
Modified subgroup.exists_finset_card_le_mulView on Github →
2022-04-20 17:09
src/group_theory/schreier.lean
feat(group_theory/schreier): Schreier's lemma in terms of `group.fg` and `group.rank` (#13361) …
Added subgroup.exists_finset_card_le_mulView on Github →