English
For m ≤ n, the coefficient of the product f g equals the coefficient of the product of truncated f and truncated g at m.
Русский
При m ≤ n коэффициент произведения f g равен коэффициенту произведения усечённых по m коэффициентов f и g.
LaTeX
$$$$ \\operatorname{coeff}_{m}(f g) = (\\operatorname{trunc'} R n f * \\operatorname{trunc'} R n g).coeff_{m} \\quad (m \\le n). $$$$
Lean4
/-- Truncation of the multivariate power series `1` -/
@[simp]
theorem trunc'_one (n : σ →₀ ℕ) : trunc' R n 1 = 1 :=
MvPolynomial.ext _ _ fun m ↦ by
classical
rw [coeff_trunc', coeff_one]
split_ifs with H H'
· subst m; simp only [MvPolynomial.coeff_zero_one]
· rw [MvPolynomial.coeff_one, if_neg (Ne.symm H')]
· rw [MvPolynomial.coeff_one, if_neg ?_]
rintro rfl
exact H (zero_le n)
