English
The collection of all scalar-formal multilinear-series on 𝕜–E–E forms a submodule of FormalMultilinearSeries 𝕜 E E. More precisely, the set { ofScalars E f | f } is closed under addition and scalar multiplication, and contains zero, hence generates a submodule of FormalMultilinearSeries 𝕜 E E.
Русский
Множество всех скалярных формальных многочленных рядов на 𝕜–E–E образует подмодуль внутри FormalMultilinearSeries 𝕜 E E. Точнее, множество { ofScalars E f | f } замкнуто относительно сложения и умножения на скаляр и содержит ноль, следовательно порождает подмодуль.
LaTeX
$$$\\text{ofScalarsSubmodule}:\\ Submodule\\ 𝕜\\ (\\mathrm{FormalMultilinearSeries}\\ 𝕜\\ E\\ E)\\quad\\text{carrier} = \\{ \\mathrm{ofScalars}\\ E\\ f \\mid f\\}$$$
Lean4
/-- The submodule generated by scalar series on `FormalMultilinearSeries 𝕜 E E`. -/
def ofScalarsSubmodule : Submodule 𝕜 (FormalMultilinearSeries 𝕜 E E)
where
carrier := {ofScalars E f | f}
add_mem' := fun ⟨c, hc⟩ ⟨c', hc'⟩ ↦ ⟨c + c', hc' ▸ hc ▸ ofScalars_add E c c'⟩
zero_mem' := ⟨0, ofScalars_series_eq_zero_of_scalar_zero 𝕜 E⟩
smul_mem' := fun x _ ⟨c, hc⟩ ↦ ⟨x • c, hc ▸ ofScalars_smul E c x⟩
