nnnorm_ratCast — Mathlib

English

The nonnegative-norm of a rational q as a complex number equals the nonnegative real q itself.

Русский

Неотрицательная норма числа q, рассмотренного как комплексное число, равна самому неотрицательному рациональному q.

LaTeX

$$$\\forall q \\in \\mathbb{Q}, \\| (q : \\mathbb{C}) \\|_{+} = \\| (q : \\mathbb{R}) \\|_{+}$$$

Lean4

@[simp 1100, norm_cast]
theorem nnnorm_ratCast (q : ℚ) : ‖(q : ℂ)‖₊ = ‖(q : ℝ)‖₊ :=
  nnnorm_real q

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