coeff_mul_eq_coeff_trunc_mul_trunc

English

If d < n, then the d-th coefficient of f·g equals the coefficient of ((trunc n f)·(trunc n g)).

Русский

Если d < n, то d-й коэффициент f·g равен коэффициенту ((trunc n f)·(trunc n g)).

LaTeX

$$$\\forall {d,n} (f,g), \\; d < n \\Rightarrow \\operatorname{coeff} d (f g) = \\operatorname{coeff} d ((\\operatorname{trunc} n f) \\cdot (\\operatorname{trunc} n g))$$$

Lean4

theorem coeff_mul_eq_coeff_trunc_mul_trunc {d n} (f g) (h : d < n) :
    coeff d (f * g) = coeff d ((trunc n f : R⟦X⟧) * (trunc n g : R⟦X⟧)) :=
  coeff_mul_eq_coeff_trunc_mul_trunc₂ f g h h

Похожие утверждения