norm_coe — Mathlib

English

For every real a, the norm of its image as a quaternion equals the absolute value of a: ∥(a : ℍ)∥ = ∥a∥.

Русский

Для любого вещественного a нормa образа a в ℍ равна абсолютному значению a: ∥(a : ℍ)∥ = ∥a∥.

LaTeX

$$$\\lVert (a : \\mathbb{H})\\rVert = \\lVert a \\rVert \\quad (a \\in \\mathbb{R}).$$$

Lean4

@[simp, norm_cast]
theorem norm_coe (a : ℝ) : ‖(a : ℍ)‖ = ‖a‖ := by
  rw [norm_eq_sqrt_real_inner, inner_self, normSq_coe, Real.sqrt_sq_eq_abs, Real.norm_eq_abs]

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