Commit 2025-06-30 14:31 e70dc4ed
View on Github →feat(Algebra/Group/Center): centralizer of product of nonempty sets (#25866) Lemma: The centralizer of the product of non-empty sets is equal to taking the product of the centralizers of the sets. I've also added a lemma for the centralizer of an empty set.