Theorems · Definition · functional analysis

constFormalMultilinearSeries

(𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_2) →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : ContinuousConstSMul 𝕜 E] →
            [inst_4 : IsTopologicalAddGroup E] →
              {F : Type u_3} →
                [inst_5 : NormedAddCommGroup F] →
                  [inst_6 : IsTopologicalAddGroup F] →
                    [inst_7 : NormedSpace 𝕜 F] → [inst_8 : ContinuousConstSMul 𝕜 F] → F → FormalMultilinearSeries 𝕜 E F

The formal multilinear series where all terms of positive degree are equal to zero, and the term of degree zero is c. It is the power series expansion of the constant function equal to c everywhere.

Defined in

Mathlib.Analysis.Calculus.FormalMultilinearSeries

Cited by

17 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceContinuousConstSMulIsTopologicalAddGroupNormedAddCommGroupIsTopologicalAddGroupNormedSpaceContinuousConstSMul