normSq_div

Mathlib.Data.Complex.Basic

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

English

Let z and w be complex numbers. Then the squared modulus of their quotient satisfies |z/w|^2 = |z|^2 / |w|^2.

Русский

Пусть z и w — комплексные числа. Тогда квадрат модуля частного удовлетворяет |z/w|^2 = |z|^2 / |w|^2.

LaTeX

$$$|z/w|^2 = \\dfrac{|z|^2}{|w|^2}$$$

Lean4

theorem normSq_div (z w : ℂ) : normSq (z / w) = normSq z / normSq w := by simp

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

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

Разделы

Аффилиация

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