Theorems · Theorem · functional analysis

ContinuousLinearMap.norm_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 norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the norms.

Defined in

Mathlib.Analysis.Normed.Operator.Bilinear

Cited by

6 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSeminormedAddCommGroupNontriviallyNormedFieldNormedSpaceNormedSpace