norm_smul_inv_norm — Mathlib

English

The norm of the extension equals the norm of the original StrongDual: ||fr.extendTo𝕜'|| = ||fr||.

Русский

Норма расширения равна норме исходного StrongDual: ||fr.extendTo𝕜'|| = ||fr||.

LaTeX

$$$\\|fr.extendTo𝕜'\\| = \\|fr\\|$$$

Lean4

/-- Lemma to normalize a vector in a normed space `E` over either `ℂ` or `ℝ` to unit length. -/
@[simp]
theorem norm_smul_inv_norm {x : E} (hx : x ≠ 0) : ‖(‖x‖⁻¹ : 𝕜) • x‖ = 1 :=
  by
  have : ‖x‖ ≠ 0 := by simp [hx]
  simp [field, norm_smul]

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