Theorem Set.Pairwise.commute_star_iff

Modification history

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