English
Let f and g be skew monoid algebra elements. Then the x-coefficient of their product is a double sum over all a1,b1 from f and a2,b2 from g, contributing b1·a1•b2 precisely when a1·a2 = x; otherwise it contributes 0.
Русский
Пусть f и g — элементы skew-монойдной алгебры. Коэффициент при x в произведении f·g равен двойному суммированию по всем a1,b1 из f и a2,b2 из g; вклад равен b1 · a1 • b2 если a1·a2 = x, иначе вклад равен 0.
LaTeX
$$$ (f * g).\mathrm{coeff}(x) = \sum_{a_1,b_1} \sum_{a_2,b_2} \mathbf{1}_{a_1 a_2 = x}\; b_1 \; (a_1 \cdot b_2) $$$
Lean4
theorem coeff_mul [DecidableEq G] (f g : SkewMonoidAlgebra k G) (x : G) :
(f * g).coeff x = f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0 :=
by
rw [mul_def, coeff_sum]; congr; ext
rw [coeff_sum]; congr; ext
exact coeff_single_apply
