English
The multiplication in MonoidAlgebra is given by a convolution-like sum of basis elements: x * y = sum over m1,r1 and m2,r2 of single (m1*m2) (r1*r2).
Русский
Умножение в MonoidAlgebra задаётся свёрткой по базисным элементам: x*y = сумма по m1,r1 и m2,r2 от single (m1*m2) (r1*r2).
LaTeX
$$$\\mathrm{mul'}\\ (x,y) = \\sum_{m_1,r_1} \\sum_{m_2,r_2} \\mathrm{single}(m_1\\cdot m_2) (r_1\\cdot r_2)$$$
Lean4
/-- The multiplication in a monoid algebra.
We make it irreducible so that Lean doesn't unfold it when trying to unify two different things. -/
@[irreducible]
def mul' (x y : MonoidAlgebra R M) : MonoidAlgebra R M :=
x.sum fun m₁ r₁ ↦ y.sum fun m₂ r₂ ↦ single (m₁ * m₂) (r₁ * r₂)
