English
For elements x, y of MonoidAlgebra R M, their product is the finitely supported function whose value at m ∈ M is the sum of x(m1) · y(m2) over all pairs m1, m2 with m1 · m2 = m.
Русский
Для элементов x, y в MonoidAlgebra R M их произведение есть конечная по опорному множеству функция, значение в m ∈ M равно сумме x(m1) · y(m2) по всем парам m1, m2 с условием m1 · m2 = m.
LaTeX
$$$ (x * y)(m) = \sum_{m_1, m_2: m_1 m_2 = m} x(m_1) \cdot y(m_2) $$$
Lean4
/-- The product of `x y : MonoidAlgebra R M` is the finitely supported function whose value at `m`
is the sum of `x m₁ * y m₂` over all pairs `m₁, m₂` such that `m₁ * m₂ = m`.
(Think of the group ring of a group.) -/
@[to_additive existing instMul]
instance instMul : Mul (MonoidAlgebra R M) where mul := mul'
