English
Let φ be a multivariate formal power series with coefficients in a commutative semiring R, indexed by σ, and let n be a finite upper bound in σ. For every index m, the coefficient of the truncated series at m equals the original coefficient at m if m < n, and is 0 otherwise.
Русский
Пусть φ — многофакторный формальный степенной ряд с коэффициентами в коммутативном полюсе R, индексируемый σ, и пусть n задаёт конечный верхний предел. Для каждого индекса m коэффициент в усечённом ряде на позиции m равен исходному коэффициенту φ_m, если m < n, иначе равен 0.
LaTeX
$$$$ \\operatorname{coeff}_{m}(\\operatorname{trunc} R n \\varphi) = \\begin{cases} \\operatorname{coeff}_{m}(\\varphi), & m < n \\\\ 0, & \\text{otherwise} \\end{cases} $$$$
Lean4
theorem coeff_trunc (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) : (trunc R n φ).coeff m = if m < n then coeff m φ else 0 := by
classical simp [trunc, coeff_truncFun]
