constantCoeff_smul — Mathlib

English

For φ in S power series and a in R, constantCoeff (a • φ) = a • constantCoeff φ.

Русский

Для φ в R⟦X⟧ и a ∈ R, константный коэффициент a • φ равен a умноженному на постоянный коэффициент φ.

LaTeX

$$$\operatorname{constantCoeff}(a \cdot \varphi) = a \cdot \operatorname{constantCoeff}(\varphi)$$$

Lean4

@[simp]
theorem constantCoeff_smul {S : Type*} [Semiring S] [Module R S] (φ : PowerSeries S) (a : R) :
    constantCoeff (a • φ) = a • constantCoeff φ :=
  rfl

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