conj_inv

Mathlib.Analysis.RCLike.Basic

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

English

The conjugate of the inverse equals the inverse of the conjugate: conj(z^{-1}) = (conj z)^{-1}.

Русский

Сопряжение обратного равно обратному сопряжённому: conj(z^{-1}) = (conj z)^{-1}.

LaTeX

$$$$ \overline{z^{-1}} = (\overline{z})^{-1}. $$$$

Lean4

@[rclike_simps]
theorem conj_inv (x : K) : conj x⁻¹ = (conj x)⁻¹ :=
  star_inv₀ _

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

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

Разделы

Аффилиация

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