Commit 2025-11-20 14:55 29507cc4

View on Github →

chore(GroupTheory/Subgroup/Centralizer): replace centralizer (zpowers s) with centralizer {s} (#30768) This PR fixes some lingering technical debt from two years ago: https://github.com/leanprover-community/mathlib3/pull/18965

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/Pointwise.lean

Modified Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean

deleted theorem Subgroup.center_eq_iInf

deleted theorem Subgroup.center_eq_infi'

deleted theorem Subgroup.centralizer_closure

Modified Mathlib/GroupTheory/Finiteness.lean

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/Index.lean

Modified Mathlib/GroupTheory/Subgroup/Centralizer.lean

added theorem Subgroup.center_eq_iInf

added theorem Subgroup.center_eq_infi'

added theorem Subgroup.centralizer_closure

added theorem Subgroup.centralizer_eq_iInf

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/Topology/Algebra/Group/SubmonoidClosure.lean

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean