English
If x is a HahnSeries and s ⊆ Γ is an IsPWO set with support conditions, then the coefficient of (x*y) at a given index a can be computed as a finite sum over an explicitly described antidiagonal depending on s, of x.coeff(i) and y.coeff(j).
Русский
Пусть x — ряд Хана, множество s удовлетворяет условию IsPWO; тогда коэффициент (x*y) в индексе a вычисляется как конечная сумма по конкретной антидиагонали, зависящей от s, коэффициентов x и y.
LaTeX
$$$ (x*y).coeff\, a = \\sum_{ij \\in \\mathrm{addAntidiagonal}\: hs\\; y.isPWO\\_support\\; a} x.coeff\, ij.fst \\cdot y.coeff\, ij.snd $$$
Lean4
theorem coeff_mul_left' [NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ} {s : Set Γ} (hs : s.IsPWO)
(hxs : x.support ⊆ s) :
(x * y).coeff a = ∑ ij ∈ addAntidiagonal hs y.isPWO_support a, x.coeff ij.fst * y.coeff ij.snd :=
HahnModule.coeff_smul_left hs hxs
