Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.rank_le_index_mul_rank

Modification history

2022-11-11 23:56
src/group_theory/schreier.lean
feat(group_theory/index): Add typeclass for `finite_index` (#17139) …
Modified subgroup.rank_le_index_mul_rankView on Github →
2022-09-03 10:46
src/group_theory/schreier.lean
refactor(group_theory/finiteness): Make `group.rank` noncomputable (#16256) …
Modified subgroup.rank_le_index_mul_rankView 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.rank_le_index_mul_rankView on Github →