English
A FormalMultilinearSeries is a family (p_n) of multilinear maps from E^n to F for each n, encoding a formal power series in several variables.
Русский
FormalMultilinearSeries — это семейство p_n из многообразно-линейных отображений E^n в F для каждого n, задающее формальную многочленную серию в нескольких переменных.
LaTeX
$$$ FormalMultilinearSeries 𝕜 E F := \forall n:\mathbb{N}, E^{\otimes n} \to_L 𝕜 F$$$
Lean4
/-- A formal multilinear series over a field `𝕜`, from `E` to `F`, is given by a family of
multilinear maps from `E^n` to `F` for all `n`. -/
@[nolint unusedArguments]
def FormalMultilinearSeries (𝕜 : Type*) (E : Type*) (F : Type*) [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E]
[TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F]
[ContinuousAdd F] [ContinuousConstSMul 𝕜 F] :=
∀ n : ℕ, E [×n]→L[𝕜] F
deriving AddCommMonoid, Inhabited
