normSq_add_mul_I

Mathlib.Data.Complex.Basic

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

English

For real x,y, normSq(x + y I) = x^2 + y^2.

Русский

Для вещественных x,y: normSq(x + yI) = x^2 + y^2.

LaTeX

$$$\operatorname{normSq}(x + y \cdot I) = x^2 + y^2$$$

Lean4

theorem normSq_add_mul_I (x y : ℝ) : normSq (x + y * I) = x ^ 2 + y ^ 2 := by rw [← mk_eq_add_mul_I, normSq_mk, sq, sq]

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

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

Разделы

Аффилиация

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