∀ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ],
  ‖ContinuousLinearMap.smulRightL 𝕜 E Fₗ‖ ≤ 1