normSq_add

Mathlib.Data.Complex.Basic

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

English

The squared modulus of a sum is given by: |z+w|^2 = |z|^2 + |w|^2 + 2 Re(z conj(w)).

Русский

Квадрат модуля суммы задаётся формулой: |z+w|^2 = |z|^2 + |w|^2 + 2 Re(z conj(w)).

LaTeX

$$$\\\\|z + w\\\\|^2 = \\\\|z\\\\|^2 + \\\\|w\\\\|^2 + 2 \\\\operatorname{Re}\\\\left(z \\\\overline{w}\\right)$$$

Lean4

theorem normSq_add (z w : ℂ) : normSq (z + w) = normSq z + normSq w + 2 * (z * conj w).re := by dsimp [normSq]; ring

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

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

Разделы

Аффилиация

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