Theorems · Definition · functional analysis

FormalMultilinearSeries

(𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : TopologicalSpace E] →
              [ContinuousAdd E] →
                [ContinuousConstSMul 𝕜 E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module 𝕜 F] →
                      [inst_8 : TopologicalSpace F] →
                        [ContinuousAdd F] → [ContinuousConstSMul 𝕜 F] → Type (max (max u_3 u_2) 0)

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.

Defined in

Mathlib.Analysis.Calculus.FormalMultilinearSeries

Cited by

615 results in Mathlib

Foundations

Depth 8 from the axioms, rests on 61 definitions · uses no axioms

Assumes

SemiringAddCommMonoidModuleTopologicalSpaceContinuousAddContinuousConstSMulAddCommMonoidModuleTopologicalSpaceContinuousAddContinuousConstSMul