nnnorm_intCast — Mathlib

English

The nonnegative norm of the complex integer n equals the nonnegative norm of n viewed as an integer, i.e., ‖(n : ℂ)‖₊ = ‖n‖₊.

Русский

Нормa неотрицательного типа для целого числа n, взятого как комплекс, равна норме для самого числа n: ‖(n : ℂ)‖₊ = ‖n‖₊.

LaTeX

$$$ \\| (n : \\mathbb{C}) \\|_{+} = \\| n \\|_{+} $$$

Lean4

@[simp 1100, norm_cast]
theorem nnnorm_intCast (n : ℤ) : ‖(n : ℂ)‖₊ = ‖n‖₊ := by ext; exact norm_intCast n

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