English
Let x be a Hahn series and y a Hahn module element. The a-th coefficient of the left smul (x acting on y) can be expressed as a finite sum over a VAddAntidiagonal, reflecting the distributive decomposition of the left action.
Русский
Пусть x — Ханнова серия и y — элемент Hahn-модуля. a-й коэффициент левого умножения (x действует на y) выражается через конечную сумму по VAddAntidiagonal, отражающую распределение левой деjkствия.
LaTeX
$$$\big( (\mathrm{of} \ R)^{-1} (x \cdot y) \big)_{a} = \sum_{(i,j) \in \mathrm{VAddAntidiagonal}} x_i \cdot ((\mathrm{of} \ R)^{-1} y)_j$$$
Lean4
theorem coeff_smul_left [SMulWithZero R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ}
(hs : s.IsPWO) (hxs : x.support ⊆ s) :
((of R).symm <| x • y).coeff a =
∑ ij ∈ VAddAntidiagonal hs ((of R).symm y).isPWO_support a, x.coeff ij.fst • ((of R).symm y).coeff ij.snd :=
by
classical
rw [coeff_smul]
apply sum_subset_zero_on_sdiff (vaddAntidiagonal_mono_left hxs) _ fun _ _ => rfl
intro b hb
simp only [not_and', mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_ne_iff] at hb
rw [hb.2 ⟨hb.1.2.1, hb.1.2.2⟩, zero_smul]
