Commit 2025-02-10 13:06 e439a5f6

View on Github →

chore(GroupTheory/Index): don't import Field (#21304)

Estimated changes

Modified Mathlib/GroupTheory/Commutator/Finite.lean

added theorem Subgroup.index_center_le_pow

Modified Mathlib/GroupTheory/Index.lean

deleted theorem Subgroup.index_center_le_pow

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/GroupTheory/Schreier.lean