conj_mul' — Mathlib

English

For any complex number z, the product of its conjugate with itself equals the square of its modulus: \\overline{z} z = |z|^2.

Русский

Для произвольного комплексного числа z произведение сопряжённого числа z на само число равно квадрату модуля: \\overline{z} z = |z|^2.

LaTeX

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

Lean4

theorem conj_mul' (z : ℂ) : conj z * z = ‖z‖ ^ 2 :=
  RCLike.conj_mul z

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