Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.finite_index_of_finite_quotient

Modification history

2022-11-11 23:56
src/group_theory/index.lean
feat(group_theory/index): Add typeclass for `finite_index` (#17139) …
Added subgroup.finite_index_of_finite_quotientView on Github →