Theorems · Definition · functional analysis

ContinuousLinearMap.mulLeftRight

(𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (R : Type u_3) →
      [inst_1 : NonUnitalSeminormedRing R] →
        [inst_2 : NormedSpace 𝕜 R] → [IsScalarTower 𝕜 R R] → [SMulCommClass 𝕜 R R] → R →L[𝕜] R →L[𝕜] R →L[𝕜] R

Simultaneous left- and right-multiplication in a non-unital normed algebra, considered as a continuous trilinear map. This is akin to its non-continuous version LinearMap.mulLeftRight, but there is a minor difference: LinearMap.mulLeftRight is uncurried.

Defined in

Mathlib.Analysis.Normed.Operator.Mul

Cited by

16 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNonUnitalSeminormedRingNormedSpaceIsScalarTowerSMulCommClass