English
Let f and g be elements of the additive-monoid algebra AddMonoidAlgebra over a semiring R on the additive monoid M. Their product is the finitely supported function defined by (f * g)(a) = sum over all x, y ∈ M with x + y = a of f(x) · g(y).
Русский
Пусть f и g — элементы алгебры Моноида AddMonoidAlgebra над кольцом R по аддитивному моноиду M. Их произведение есть конечная по опорному множеству функция: (f * g)(a) = сумма по всем x, y ∈ M such что x + y = a от f(x) · g(y).
LaTeX
$$$ (f * g)(a) = \sum_{x+y=a} f(x) \; g(y) $$$
Lean4
/-- The product of `f g : k[G]` is the finitely supported function
whose value at `a` is the sum of `f x * g y` over all pairs `x, y`
such that `x + y = a`. (Think of the product of multivariate
polynomials where `α` is the additive monoid of monomial exponents.) -/
instance _root_.AddMonoidAlgebra.instMul [Add M] : Mul (AddMonoidAlgebra R M) where
mul f g := MonoidAlgebra.mul' (M := Multiplicative M) f g
