norm_real

Mathlib.Analysis.Complex.Norm

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

English

For any real r, viewed as a complex number, ‖r‖ = |r|.

Русский

Для вещественного r, рассматриваемого как комплексное число, ‖r‖ = |r|.

LaTeX

$$$\forall r \in \mathbb{R},\; \|r\|_{\mathbb{C}} = |r|$$$

Lean4

@[simp 1100, norm_cast]
theorem norm_real (r : ℝ) : ‖(r : ℂ)‖ = ‖r‖ := by simp [norm_def, Real.sqrt_mul_self_eq_abs]

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

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

Разделы

Аффилиация

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