coeff_mul_C — Mathlib

English

For n ∈ ℕ, φ ∈ R⟦X⟧, a ∈ R, the nth coefficient of φ times the constant series C a equals coeff n φ times a.

Русский

Для n ∈ ℕ, φ ∈ R⟦X⟧, a ∈ R, n-й коэффициент произведения φ на константный ряд C a равен coeff n φ умноженное на a.

LaTeX

$$$\operatorname{coeff}_n(\varphi \cdot C a) = \operatorname{coeff}_n(\varphi) \cdot a$$$

Lean4

@[simp]
theorem coeff_mul_C (n : ℕ) (φ : R⟦X⟧) (a : R) : coeff n (φ * C a) = coeff n φ * a :=
  MvPowerSeries.coeff_mul_C _ φ a

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