subst_smul — Mathlib

English

A variant of the finite-support property for substituted coefficients, with b as the substituting series.

Русский

Вариант свойства конечной поддержки подстановочных коэффициентов с b как подстановочным рядом.

LaTeX

$$$\forall hb\, (f : PowerSeries R)\, (e : \mathbb{N}),\ Finite\left(\{ d \mid coeff_d f · coeff_e (b^d) \}\right)$$$

Lean4

theorem subst_smul [Algebra A S] [IsScalarTower A R S] (ha : HasSubst a) (r : A) (f : PowerSeries R) :
    subst a (r • f) = r • (subst a f) := by rw [← coe_substAlgHom ha, AlgHom.map_smul_of_tower]

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