coeff_smul — Mathlib

English

For any f in the mv-power-series ring and any index n, the n-th coefficient is linear in the scalar: coeff n (a · f) = a · coeff n f.

Русский

Для любой f в кольце mv-порядков и любого индекса n тождество: coeff n (a · f) = a · coeff n f.

LaTeX

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

Lean4

@[simp]
theorem coeff_smul (f : MvPowerSeries σ R) (n) (a : R) : coeff n (a • f) = a * coeff n f :=
  rfl

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