English
For HahnSeries x, y with coefficients in a semiring R, the coefficient at a given index a in the product x*y is the finite sum over all pairs (i,j) whose additive index equals a, of x.coeff(i) · y.coeff(j).
Русский
Для рядов Хана x, y с коэффициентами в полупринуждённом полугруппе R коэффициент при индексе a в произведении x*y равен сумме по всем парам (i,j), удовлетворяющим i+j=a, из x.coeff(i) · y.coeff(j).
LaTeX
$$$ (x*y).\\mathrm{coeff}\, a = \\sum_{ij \\in \\mathrm{addAntidiagonal}\\; x.isPWO\\_support\\; y.isPWO\\_support\\; a} x.coeff\, ij.fst \\cdot y.coeff\, ij.snd $$$
Lean4
theorem coeff_mul [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ} :
(x * y).coeff a = ∑ ij ∈ addAntidiagonal x.isPWO_support y.isPWO_support a, x.coeff ij.fst * y.coeff ij.snd :=
rfl
