norm_int_of_nonneg

Mathlib.Analysis.Complex.Norm

URI: https://scilib.ai/kg/mathlib#Complex.norm_int_of_nonneg

English

If n ∈ ℤ and n ≥ 0, then ‖n‖ = n.

Русский

Если n ∈ ℤ и n ≥ 0, то ‖n‖ = n.

LaTeX

$$$\forall n \in \mathbb{Z},\; n \ge 0 \Rightarrow \|n\| = n$$$

Lean4

theorem norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) : ‖(n : ℂ)‖ = n := by
  rw [norm_intCast, ← Int.cast_abs, abs_of_nonneg hn]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru