Commit 2025-04-14 19:01 a1fe861b

View on Github →

refactor: rename FiniteIndex.finiteIndex to index_ne_zero (#24044)

Estimated changes

Modified Mathlib/GroupTheory/CosetCover.lean

Modified Mathlib/GroupTheory/Index.lean

Modified Mathlib/GroupTheory/Schreier.lean

Modified Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean