English
The coefficient equality for products under trunc' holds with the same hypotheses as in the non-primed version.
Русский
Коэффициентное равенство для произведений в усечении сохраняется при тех же предпосылках, что и без primed.
LaTeX
$$$$ \\operatorname{coeff}_{m}(f g) = (\\operatorname{trunc'} R n f * \\operatorname{trunc'} R n g).coeff_{m} \\quad (m \\le n). $$$$
Lean4
/-- Coefficients of the truncation of a product of two multivariate power series -/
theorem coeff_mul_eq_coeff_trunc'_mul_trunc' (n : σ →₀ ℕ) (f g : MvPowerSeries σ R) {m : σ →₀ ℕ} (h : m ≤ n) :
coeff m (f * g) = (trunc' R n f * trunc' R n g).coeff m := by
classical
simp only [MvPowerSeries.coeff_mul, MvPolynomial.coeff_mul]
apply Finset.sum_congr rfl
rintro ⟨i, j⟩ hij
simp only [mem_antidiagonal] at hij
rw [← hij] at h
simp only
apply congr_arg₂
· rw [coeff_trunc', if_pos (le_trans le_self_add h)]
· rw [coeff_trunc', if_pos (le_trans le_add_self h)]
