English
Let x be a Hahn series and y a Hahn module element. For a ∈ Γ′ and a suitable finite set s with a well-ordered property, the a-th coefficient of the right smul (of R)^{-1} applied to x and y is given by a finite sum over pairs (i, j) in the VAddAntidiagonal, namely x_i · y_j.
Русский
Пусть x — Ханнова серия и y — элемент Hahn-модуля. Для a ∈ Γ′ и подходящего конечного множества s с хорошо упорядоченным свойством, a-й коэффициент правого умножения (обратного) x на y задаётся конечной суммой по парам (i, j) в VAddAntidiagonal: x_i · y_j.
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_right [SMulZeroClass R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ'}
(hs : s.IsPWO) (hys : ((of R).symm y).support ⊆ s) :
((of R).symm <| x • y).coeff a =
∑ ij ∈ VAddAntidiagonal x.isPWO_support hs 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_right hys) _ fun _ _ => rfl
intro b hb
simp only [not_and, mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_imp_not] at hb
rw [hb.2 hb.1.1 hb.1.2.2, smul_zero]
