nnnorm_natCast

Mathlib.Analysis.Complex.Norm

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

English

The nonnegative norm of n cast equals n: ‖n‖₊ = n.

Русский

Ненегативная норма числа n в представлении равна n: ‖n‖₊ = n.

LaTeX

$$$\|n\|_{+} = n$$$

Lean4

@[simp 1100, norm_cast]
theorem nnnorm_natCast (n : ℕ) : ‖(n : ℂ)‖₊ = n :=
  Subtype.ext <| by simp [norm_natCast]

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

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

Разделы

Аффилиация

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