Commit 2024-05-01 01:21 85a4f8e9

feat: make multiplication in [Add]MonoidAlgebra irreducible (#12554)

• See Zulip
• The example in that thread takes ~55000ms on master and 43ms on this branch.
• I expect that this will lead to little gains in the (working) proofs of Mathlib.
• The multiplication on MonoidAlgebra _ G and AddMonoidAlgebra _ (Additive G) are still defeq the same.