norm_ratCast — Mathlib

English

Let q be any rational number. Then the modulus of q considered as a complex number equals the real absolute value of q: ||(q) in C|| = |q| in R.

Русский

Пусть q — произвольное рациональное число. Тогда модуль q, воспринятый как комплексное число, равен абсолютному значению q на действительной оси: ∥(q)∈ℂ∥ = |q|.

LaTeX

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

Lean4

@[simp 1100, norm_cast]
theorem norm_ratCast (q : ℚ) : ‖(q : ℂ)‖ = |(q : ℝ)| :=
  norm_real _

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