Commit 2024-11-17 15:35 32240b25

feat: the bicentralizer of a commutative set is commutative (#18700) This shows that the bicentralizer (a.k.a. bicommutant) of a commutative set is commutative. Moreover, since s ⊆ s.centralizer.centralizer, if s is a commutative set, then closure s ≤ centralizer (centralizer s) for various subobject closures. Consequently, we obtain simplified proofs that if s is commutative, then so is closure s.