norm_smulRightL — Mathlib

English

The norm of smulRightL by a strong dual element equals the norm of that element.

Русский

Норма smulRightL по сильному двойственному элементу равна норме этого элемента.

LaTeX

$$$\\|smulRightL\\, 𝕜\\, E\\, F_\\ell\\, c\\| = \\|c\\|$ for c in the dual space.$$

Lean4

@[simp]
theorem norm_smulRightL (c : StrongDual 𝕜 E) [Nontrivial Fₗ] : ‖smulRightL 𝕜 E Fₗ c‖ = ‖c‖ :=
  ContinuousLinearMap.homothety_norm _ c.norm_smulRight_apply

Похожие утверждения