conj_mul

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.conj_mul

English

The product of the conjugate with the number equals the square of the norm, symmetric in order.

Русский

Произведение сопряжённого и числа равно квадрату нормы, не зависит от порядка.

LaTeX

$$$$\\overline{z} \\cdot z = \\|z\\|^{2}.$$$$

Lean4

theorem conj_mul (z : K) : conj z * z = ‖z‖ ^ 2 := by rw [mul_comm, mul_conj]

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

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

Разделы

Аффилиация

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