Theorems · Theorem · functional analysis

ContinuousLinearMap.nnnorm_smulRight_apply

∀ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] (c : StrongDual 𝕜 E)
  (f : Fₗ), ‖ContinuousLinearMap.smulRight c f‖₊ = ‖c‖₊ * ‖f‖₊

The non-negative norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the non-negative norms.

Defined in

Mathlib.Analysis.Normed.Operator.Bilinear

Cited by

0 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupNontriviallyNormedFieldNormedSpaceNormedSpace