Theorem Subgroup.index_eq_sum_minimalPeriod

Modification history

2026-02-26 14:02
Mathlib/Data/ZMod/QuotientGroup.lean
feat(GroupTheory/Focal): add focal subgroup theorem (#34380) …
Added Subgroup.index_eq_sum_minimalPeriodView on Github →