inv_eq_conj

Mathlib.Analysis.Complex.Basic

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

English

If a complex number z has modulus 1, then its inverse equals its complex conjugate: z^{-1} = \\overline{z}.

Русский

Если модули z равен 1, тогда обратное числа z равно его комплексному сопряжённому: z^{-1} = \\overline{z}.

LaTeX

$$$\\\\lVert z\\\\rVert = 1 \\\\Rightarrow z^{-1} = \\\\overline{z}$$$

Lean4

theorem inv_eq_conj (hz : ‖z‖ = 1) : z⁻¹ = conj z :=
  RCLike.inv_eq_conj hz

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

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

Разделы

Аффилиация

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