English
For x, y ∈ MonoidAlgebra R M and m ∈ M, the coefficient (x*y)(m) equals the sum over all m1, m2 with m1*m2=m of x(m1)·y(m2), equivalently via indicator: (x*y)(m) = ∑_{m1,m2} x(m1) y(m2) if m1 m2 = m, else 0.
Русский
Для x, y ∈ MonoidAlgebra R M и m ∈ M коэффициент (x*y)(m) равен сумме по всем m1,m2 с условием m1 m2 = m от x(m1)·y(m2); иначе 0.
LaTeX
$$$ (x * y)(m) = \sum_{m_1,m_2} x(m_1) y(m_2) \;\text{при } m_1 m_2 = m \quad \text{(равно 0, если не выполняется)} $$$
Lean4
@[to_additive (dont_translate := R) mul_apply]
theorem mul_apply [DecidableEq M] (x y : MonoidAlgebra R M) (m : M) :
(x * y) m = x.sum fun m₁ r₁ ↦ y.sum fun m₂ r₂ ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 := by
-- Porting note: `reducible` cannot be `local` so proof gets long.
rw [mul_def, Finsupp.sum_apply]; congr; ext
rw [Finsupp.sum_apply]; congr; ext
apply single_apply
