Commit 2026-10-17 18:35 d70b73b4

View on Github →

feat: lemmas for subgroups of finite index (#44957)

Estimated changes

Modified Mathlib/GroupTheory/Index.lean

added theorem Subgroup.finiteIndex_bot_iff

added theorem Subgroup.index_ne_zero

added theorem Subgroup.index_pos

modified theorem Subgroup.relIndex_ne_zero

added theorem Subgroup.relIndex_pos

Modified Mathlib/GroupTheory/IndexNSmul.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/GroupTheory/Schreier.lean

Modified Mathlib/NumberTheory/NumberField/Units/Regulator.lean