conj_inv

Mathlib.Data.Complex.Basic

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

English

For every x ∈ ℂ, conj(x⁻¹) = (conj x)⁻¹.

Русский

Для любого x ∈ ℂ сопряжённое к обратному равно обратному к сопряжённому: conj(x⁻¹) = (conj x)⁻¹.

LaTeX

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

Lean4

theorem conj_inv (x : ℂ) : conj x⁻¹ = (conj x)⁻¹ :=
  star_inv₀ _

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

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

Разделы

Аффилиация

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