norm_nnratCast — Mathlib

English

For every nonnegative rational q, the modulus of q in the complex plane equals q itself.

Русский

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

LaTeX

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

Lean4

@[simp 1100, norm_cast]
theorem norm_nnratCast (q : ℚ≥0) : ‖(q : ℂ)‖ = q :=
  Complex.norm_of_nonneg q.cast_nonneg

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