English
There is a canonical way to view a formal 𝕜′-multilinear series as a formal 𝕜-multilinear series by restricting scalars on each coefficient. Concretely, for any p : FormalMultilinearSeries 𝕜′ E F, define restrictScalars 𝕜 p by (restrictScalars 𝕜 p)(n) = (p(n)).restrictScalars 𝕜. This yields a formal multilinear series from E to F over 𝕜.
Русский
Существует естественное преобразование, переводящее формальную линейно-многочленную последовательность над полем 𝕜′ в формальную линейно-многочленную последовательность над полем 𝕜 путём ограничения скаляров на каждое слагаемое. Пусть p : FormalMultilinearSeries 𝕜′ E F. Тогда задаём restrictScalars 𝕜 p по (restrictScalars 𝕜 p)(n) = (p(n)).restrictScalars 𝕜; это даёт формальную multilinear-ряд над 𝕜 от E к F.
LaTeX
$$$\\text{restrictScalars}_{\\mathbb{K}}^{\\mathbb{K}'}(p)_n = (p(n)).\\restrictScalars \\mathbb{K}$$$
Lean4
/-- Reinterpret a formal `𝕜'`-multilinear series as a formal `𝕜`-multilinear series. -/
@[simp]
protected def restrictScalars (p : FormalMultilinearSeries 𝕜' E F) : FormalMultilinearSeries 𝕜 E F := fun n =>
(p n).restrictScalars 𝕜
