norm_add_mul_I

Mathlib.Analysis.Complex.Norm

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

English

For real x and y, the norm of x + y i equals sqrt(x^2 + y^2).

Русский

Для действительных x и y норма x + y i равна sqrt(x^2 + y^2).

LaTeX

$$$\\forall x,y \\in \\mathbb{R}, \\| x + y \\cdot i \\| = \sqrt{ x^{2} + y^{2} }$$$

Lean4

theorem norm_add_mul_I (x y : ℝ) : ‖x + y * I‖ = √(x ^ 2 + y ^ 2) := by rw [← normSq_add_mul_I]; rfl

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

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

Разделы

Аффилиация

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