norm_intCast

Mathlib.Analysis.Complex.Norm

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

English

For any integer n, the norm equals the absolute value of n: ‖n‖ = |n|.

Русский

Для любого целого числа n норма равна модулю числа: ‖n‖ = |n|.

LaTeX

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

Lean4

@[simp 1100, norm_cast]
theorem norm_intCast (n : ℤ) : ‖(n : ℂ)‖ = |(n : ℝ)| := by rw [← ofReal_intCast, norm_real, Real.norm_eq_abs]

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

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

Разделы

Аффилиация

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