conj_conj

Mathlib.Analysis.Complex.UnitDisc.Basic

URI: https://scilib.ai/kg/mathlib#Complex.UnitDisc.conj_conj

English

Conjugation on the unit disc is an involution: conj(conj z) = z for all z in 𝔻.

Русский

Сопряжение на единичном диске — инволюция: conj(conj z) = z для всех z ∈ 𝔻.

LaTeX

$$$\forall z \in \mathbb{D}, \operatorname{conj}(\operatorname{conj}(z)) = z$$$

Lean4

@[simp]
theorem conj_conj (z : 𝔻) : conj (conj z) = z :=
  coe_injective <| Complex.conj_conj (z : ℂ)

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

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

Разделы

Аффилиация

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