Theorems · Definition · functional analysis

NonUnitalAlgHom.Lmul

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

Multiplication on the left in a non-unital normed algebra R as a non-unital algebra homomorphism into the algebra of continuous linear maps. This is the left regular representation of A acting on itself. This has more algebraic structure than ContinuousLinearMap.mul, but there is no longer continuity bundled in the first coordinate. An alternative viewpoint is that this upgrades NonUnitalAlgHom.lmul from a homomorphism into linear maps to a homomorphism into continuous linear maps.

Defined in

Mathlib.Analysis.Normed.Operator.Mul

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNonUnitalSeminormedRingNormedSpaceIsScalarTowerSMulCommClass