ofScalars_apply_eq' — Mathlib

English

The nth coefficient map has the form that the coefficient map commutes with the scalar multiplication, i.e., (ofScalars E c n) is linear in c(n).

Русский

Н-й коэффициентный маппинг сохраняет умножение на скаляры в коэффициенте: (ofScalars E c n) линейна по c(n).

LaTeX

$$$\forall n,\ (\operatorname{ofScalars} E (x\cdot c))_n = x\cdot (\operatorname{ofScalars} E c)_n$$$

Lean4

/-- This naming follows the convention of `NormedSpace.expSeries_apply_eq'`. -/
theorem ofScalars_apply_eq' (x : E) : (fun n ↦ ofScalars E c n (fun _ ↦ x)) = fun n ↦ c n • x ^ n := by simp [ofScalars]

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