Commit 2025-04-10 07:25 8a90888b

chore(GroupTheory): Add the class IsMulCommutative (#23773) This PR adds the class IsMulCommutative α extending Mul α and stating that the multiplication is a commutative operation, and the instances that promote a Monoid or a Group to a CommMonoid or a CommGroup if it satisfies IsMulCommutative (and also the additive version). This allows to delete the class Subgroup.IsCommutative. There is no attempt to add instances to promote Monoid, GroupWithZero, MonoidWithZero, etc. to their Comm counterparts using IsMulCommutative since these come with a price and there is no use for those at the moment whereas the group version will be useful to work with Abelian Galois extensions, for example.