Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subgroup.finite_index_of_le

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_leView on Github →