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]