English
If the nth index is below the order of ψ, then the nth coefficient of φ·(1−ψ) equals the nth coefficient of φ.
Русский
Если n-м индекс меньше order(ψ), то коэффициент n у φ·(1−ψ) равен коэффициенту n у φ.
LaTeX
$$$\operatorname{coeff}_n(\phi\cdot(1-\psi)) = \operatorname{coeff}_n(\phi) \quad\text{if } ↑n < \operatorname{order}(\psi)$$$
Lean4
/-- If `n` is strictly smaller than the order of `ψ`, then the `n`th coefficient of its product
with any other power series is `0`. -/
theorem coeff_mul_of_lt_order {φ ψ : R⟦X⟧} {n : ℕ} (h : ↑n < ψ.order) : coeff n (φ * ψ) = 0 :=
by
suffices coeff n (φ * ψ) = ∑ p ∈ antidiagonal n, 0 by rw [this, Finset.sum_const_zero]
rw [coeff_mul]
apply Finset.sum_congr rfl
intro x hx
refine mul_eq_zero_of_right (coeff x.fst φ) (coeff_of_lt_order x.snd (lt_of_le_of_lt ?_ h))
rw [mem_antidiagonal] at hx
norm_cast
cutsat
