coeff_ofScalars — Mathlib

English

The nth coefficient map of the scalar series is exactly the nth coefficient function: (ofScalars E c).coeff n = c n for any n, under a suitable normed setting.

Русский

n-й коэффициент формальной скалярной серии равен точно c(n): (ofScalars E c).coeff n = c(n).

LaTeX

$$$\forall n:\mathbb{N},\ (\operatorname{ofScalars} E c).\mathrm{coeff}\ n = c(n)$$$

Lean4

@[simp]
theorem coeff_ofScalars {𝕜 : Type*} [NontriviallyNormedField 𝕜] {p : ℕ → 𝕜} {n : ℕ} :
    (FormalMultilinearSeries.ofScalars 𝕜 p).coeff n = p n := by
  simp [FormalMultilinearSeries.coeff, FormalMultilinearSeries.ofScalars, List.prod_ofFn]

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