Commit 2023-12-03 23:47 ee87d34d

refactor(Algebra/Group/Defs): Separate commutative and associative multiplication (addition) (#7060) Currently in Mathlib there is no class for magma that are commutative but not associative - Field extends CommRing and DivisionRing, CommRing extends Ring and CommMonoid, CommGroup extends Group and CommMonoid and CommMonoid extends CommSemigroup and Monoid. CommSemigroup currently extends only Semigroup and has mul_comm as a property. This PR moves mul_comm into a new CommMagma (AddCommMagma) class which extends Mul (Add). CommSemigroup now extends Semigroup and CommMagma. The rest of Mathlib4 compiles as before, except with the need to increase synthInstance.maxHeartbeats for lift_of_splits. (Update: The linter is objecting to an unused argument in what seems to be a completely unrelated bit of code (AddEquiv.lpPiLp). Trying a nolint for now.) Also referenced in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60add_comm.60.20without.20.60add_assoc.60