mathlib

307711e2 - feat(group_theory/general_commutator): subgroup.pi commutes with the general_commutator (#11825)