Theorem Set.Pairwise.commute_union_star_self_iff

Modification history

2026-09-07 07:56
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
refactor: use `Set.Pairwise s Commute` for commutativity of subobject closures (#42804) …
Added Set.Pairwise.commute_union_star_self_iffView on Github →