norm_conj

Mathlib.Analysis.Complex.Norm

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

English

The modulus is invariant under complex conjugation: ‖conj z‖ = ‖z‖.

Русский

Модуль сохраняется под комплексно сопряжением: ‖conj z‖ = ‖z‖.

LaTeX

$$$\forall z \in \mathbb{C},\; \|\overline{z}\| = \|z\|$$$

Lean4

theorem norm_conj (z : ℂ) : ‖conj z‖ = ‖z‖ := by simp [norm_def]

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

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

Разделы

Аффилиация

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