Theorem Set.centralizer_empty

Modification history

2026-01-14 09:35
Mathlib/Algebra/Group/Center.lean
chore(Algebra/Group/Center): golf some stuff (#33828)
Modified Set.centralizer_emptyView on Github →
2025-06-30 14:31
Mathlib/Algebra/Group/Center.lean
feat(Algebra/Group/Center): centralizer of product of nonempty sets (#25866) …
Added Set.centralizer_emptyView on Github →