constantCoeff_subst — Mathlib

English

If a substitution a has HasSubst, then the constant term of subst a f equals the finite sum over d ≥ 0 of coeff d f times the constant term of a^d.

Русский

Если подстановка a удовлетворяет условию HasSubst, то константный коэффициент подстановки a в f равен сумме по d ≥ 0 коэффициента d от f, умноженного на константный коэффициент a^d.

LaTeX

$$$\\operatorname{constantCoeff}(\\operatorname{subst}\\ a\ \\, f) = \\sum_{d \\ge 0} \\operatorname{coeff}_d f \\cdot \\operatorname{constantCoeff}(a^d)$$$

Lean4

theorem constantCoeff_subst (ha : HasSubst a) (f : PowerSeries R) :
    MvPowerSeries.constantCoeff (subst a f) = finsum (fun d ↦ coeff d f • MvPowerSeries.constantCoeff (a ^ d)) := by
  simp only [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply, coeff_subst ha f 0]

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