norm_cast_real — Mathlib

English

The norm of a rational cast to real equals the real norm of the real value.

Русский

Норма рационального числа после приведения к ℝ равна норме соответствующего вещественного значения.

LaTeX

$$$\\|r\\|_{ℝ} = \\|r\\|_{ℚ}$$$

Lean4

@[norm_cast, simp high] -- increase priority to prevent the left-hand side from simplifying

theorem norm_cast_real (r : ℚ) : ‖(r : ℝ)‖ = ‖r‖ :=
  rfl

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