Commit 2026-01-14 09:35 e2a36edc

View on Github →

chore(Algebra/Group/Center): golf some stuff (#33828)

Estimated changes

Modified Mathlib/Algebra/Group/Center.lean

modified theorem Set.centralizer_empty

modified theorem Set.subset_centralizer_centralizer