Theorems · Definition · several complex variables

FormalMultilinearSeries.id

(𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → E → FormalMultilinearSeries 𝕜 E E

The identity formal multilinear series, with all coefficients equal to 0 except for n = 1 where it is (the continuous multilinear version of) the identity. We allow an arbitrary constant coefficient x.

Defined in

Mathlib.Analysis.Analytic.Composition

Cited by

10 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace