mathlib

b7360f94 - feat(group_theory/general_commutator): subgroup.prod commutes with the general_commutator (#11818)