nnnorm_nnratCast — Mathlib

English

For every nonnegative rational q, the nonnegative-norm of q regarded as a complex is exactly q.

Русский

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

LaTeX

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

Lean4

@[simp 1100, norm_cast]
theorem nnnorm_nnratCast (q : ℚ≥0) : ‖(q : ℂ)‖₊ = q := by simp [nnnorm]

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