English
The coefficient of the product (of R)^{-1}(x • y) at a is a sum over the VAddAntidiagonal of x and y involving coefficients, i.e., the standard coefficient formula for the product under the defined SMul.
Русский
Коэффициент произведения (of R)^{-1}(x • y) при a выражается как сумма по VAddAntidiagonal x и y с участием коэффициентов, являясь стандартной формулой коэффициентов произведения.
LaTeX
$$$((of\,R).symm \lvert x \cdot y\rvert).coeff\ a = \sum_{ij \in VAddAntidiagonal\,x.isPWO\_support\,((of\,R).symm\,y).isPWO\_support\ a} x.coeff i.fst \cdot ((of\,R).symm\,y).coeff i.snd$$$
Lean4
theorem coeff_smul (x : HahnSeries Γ R) (y : HahnModule Γ' R V) (a : Γ') :
((of R).symm <| x • y).coeff a =
∑ ij ∈ VAddAntidiagonal x.isPWO_support ((of R).symm y).isPWO_support a,
x.coeff ij.fst • ((of R).symm y).coeff ij.snd :=
rfl
