Theorem Set.centralizer_centralizer_pairwise_commute

Modification history

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