Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.fg_of_index_ne_zero

Modification history

2022-11-11 23:56
src/group_theory/schreier.lean
feat(group_theory/index): Add typeclass for `finite_index` (#17139) …
Deleted subgroup.fg_of_index_ne_zeroView 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.fg_of_index_ne_zeroView on Github →