English
If n < a and n < b, then the n-th coefficient of f·g equals the n-th coefficient of (trunc a f)·(trunc b g).
Русский
Если n < a и n < b, то n-й коэффициент f·g равен n-му коэффициенту (trunc a f)·(trunc b g).
LaTeX
$$$\\forall {n a b} (f g : R⟦X⟧), (n < a) → (n < b) → \\operatorname{coeff} n (f g) = \\operatorname{coeff} n ((\\operatorname{trunc} a f) \\cdot (\\operatorname{trunc} b g))$$$
Lean4
/-- The `n`-th coefficient of `f*g` may be calculated
from the truncations of `f` and `g`. -/
theorem coeff_mul_eq_coeff_trunc_mul_trunc₂ {n a b} (f g : R⟦X⟧) (ha : n < a) (hb : n < b) :
coeff n (f * g) = coeff n ((trunc a f : R⟦X⟧) * (trunc b g : R⟦X⟧)) :=
by
symm
rw [← coeff_coe_trunc_of_lt n.lt_succ_self, ← trunc_trunc_mul_trunc, trunc_trunc_of_le f ha, trunc_trunc_of_le g hb,
trunc_trunc_mul_trunc, coeff_coe_trunc_of_lt n.lt_succ_self]
