constantCoeff_subst — Mathlib

English

The constant term of the substituted series is the finite sum of the products of coefficients of f with the constant coefficients of the substituted monomials.

Русский

Постоянный коэффициент подстановки равен конечной сумме произведений коэффициентов f и констант подстановок мономиалов.

LaTeX

$$$\\operatorname{constantCoeff}(\\operatorname{subst}(a,f)) = \\operatorname{finsum}( d \\mapsto \\operatorname{coeff}_{d} f \\cdot \\operatorname{constantCoeff}(d.\\prod (a_s)^e) )$$$

Lean4

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

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