Theorems · Definition · functional analysis

ContinuousMultilinearMap.piFieldEquiv

(𝕜 : Type u) →
  (ι : Type v) →
    (G : Type wG) →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup G] →
          [inst_2 : NormedSpace 𝕜 G] → [inst_3 : Fintype ι] → G ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun x => 𝕜) G

Continuous multilinear maps on 𝕜^n with values in G are in bijection with G, as such a continuous multilinear map is completely determined by its value on the constant vector made of ones. We register this bijection as a linear isometry in ContinuousMultilinearMap.piFieldEquiv.

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Basic

Cited by

15 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpaceFintype