Theorem Set.prod_centralizer_subset_centralizer_prod

Modification history

2025-06-30 14:31
Mathlib/Algebra/Group/Center.lean
feat(Algebra/Group/Center): centralizer of product of nonempty sets (#25866) …
Added Set.prod_centralizer_subset_centralizer_prodView on Github →