English
The coefficient of a product (b,r) • x at b+a equals r times the coefficient of x at a.
Русский
Коэффициент произведения (b,r)•x на позиции b+a равен r умножить на коэффициент x на позиции a.
LaTeX
$$$\\big((\\mathrm{HahnSeries.single } b r) \\cdot x\\big).coeff\\,(b+a) = r \\cdot x.coeff\\, a$$$
Lean4
theorem coeff_single_smul_vadd [MulZeroClass R] [SMulWithZero R V] {r : R} {x : HahnModule Γ' R V} {a : Γ'} {b : Γ} :
((of R).symm (HahnSeries.single b r • x)).coeff (b +ᵥ a) = r • ((of R).symm x).coeff a :=
by
by_cases hr : r = 0
· simp_all only [map_zero, zero_smul, coeff_smul, HahnSeries.support_zero, HahnSeries.coeff_zero, sum_const_zero]
simp only [hr, coeff_smul, coeff_smul, HahnSeries.support_single_of_ne, ne_eq, not_false_iff]
by_cases hx : ((of R).symm x).coeff a = 0
· simp only [hx, smul_zero]
rw [sum_congr _ fun _ _ => rfl, sum_empty]
ext ⟨a1, a2⟩
simp only [notMem_empty, not_and, Set.mem_singleton_iff, mem_vaddAntidiagonal, iff_false]
rintro rfl h2 h1
rw [IsCancelVAdd.left_cancel a1 a2 a h1] at h2
exact h2 hx
trans ∑ ij ∈ {(b, a)}, (HahnSeries.single b r).coeff ij.fst • ((of R).symm x).coeff ij.snd
· apply sum_congr _ fun _ _ => rfl
ext ⟨a1, a2⟩
simp only [Set.mem_singleton_iff, Prod.mk_inj, mem_vaddAntidiagonal, mem_singleton]
constructor
· rintro ⟨rfl, _, h1⟩
exact ⟨rfl, IsCancelVAdd.left_cancel a1 a2 a h1⟩
· rintro ⟨rfl, rfl⟩
exact ⟨rfl, by exact hx, rfl⟩
· simp
