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]