Commit 2026-09-07 07:56 b2fa0e28

refactor: use Set.Pairwise s Commute for commutativity of subobject closures (#42804) Given the subobject closure s generated by a set s, to ensure IsMulCommutative s, Mathlib assumed ∀ x ∈ s, ∀ y ∈ s, x * y = y * x, but it suffices to prove s.Pairwise Commute and this gives us access to some API. This PR switches those hypotheses. For star algebras, we switch from ∀ x ∈ s, ∀ y ∈ s, x * y = y * x and ∀ x ∈ s, ∀ y ∈ s, x * star y = star y * x to a collection of three hypotheses: ∀ x ∈ s, IsStarNormal x, s.Pairwise Commute and s.Pairwise (Commute · <| star ·). Even though this is three separate hypotheses, we claim that in practice these are the more natural conditions (except in the trivial case when the ambient algebra is commutative, but that's not the point of IsMulCommutative anyway). Moreover, we use Fuglede's theorem to conclude s.Pairwise (Commute · <| star ·) from the other two hypotheses in C⋆-algebras. Along the way, we add a variety of convenience lemmas for Set.Pairwise, including its various interactions with commutativity and star. In particular, we characterize (s ∪ star s).Pairwise Commute as the conjunction of s.Pairwise Commute, s.Pairwise (Commute · <| star ·) and ∀ x ∈ s, IsStarNormal x. This allows for a few simplifications.