English
Convolution with a single-term series acts by multiplying the corresponding coefficient by r and shifting by b.
Русский
Свёртка с одиночным рядом действует умножением соответствующего коэффициента на r и сдвигом на b.
LaTeX
$$$ (x \cdot \mathrm{single}\; b\; r)_{a+b} = x_a \cdot r $$$
Lean4
theorem coeff_mul_single_add [NonUnitalNonAssocSemiring R] {r : R} {x : HahnSeries Γ R} {a : Γ} {b : Γ} :
(x * single b r).coeff (a + b) = x.coeff a * r :=
by
by_cases hr : r = 0
· simp [hr, coeff_mul]
simp only [hr, coeff_mul, support_single_of_ne, Ne, not_false_iff]
by_cases hx : x.coeff a = 0
· simp only [hx, zero_mul]
rw [sum_congr _ fun _ _ => rfl, sum_empty]
ext ⟨a1, a2⟩
simp only [notMem_empty, not_and, Set.mem_singleton_iff, mem_addAntidiagonal, iff_false]
rintro h2 rfl h1
rw [← add_right_cancel h1] at hx
exact h2 hx
trans ∑ ij ∈ {(a, b)}, x.coeff ij.fst * (single b r).coeff ij.snd
· apply sum_congr _ fun _ _ => rfl
ext ⟨a1, a2⟩
simp only [Set.mem_singleton_iff, Prod.mk_inj, mem_addAntidiagonal, mem_singleton]
constructor
· rintro ⟨_, rfl, h1⟩
exact ⟨add_right_cancel h1, rfl⟩
· rintro ⟨rfl, rfl⟩
simp [hx]
· simp
