Theorems · Definition · functional analysis

ContinuousMultilinearMap.smulRightL

(𝕜 : Type u) →
  {ι : Type v} →
    (E : ι → Type wE) →
      (G : Type wG) →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] →
                  [Fintype ι] → ContinuousMultilinearMap 𝕜 E 𝕜 →L[𝕜] G →L[𝕜] ContinuousMultilinearMap 𝕜 E G

Continuous bilinear map realizing (f, z) ↦ f.smulRight z.

Defined in

Mathlib.Analysis.Normed.Module.Multilinear.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpaceSeminormedAddCommGroupNormedSpaceFintype