conjCLE — Mathlib

English

The conjugation map induces a real-linear continuous isomorphism of ℂ with itself.

Русский

Сопряжение задаёт непрерывное ℝ-линейное биективное отображение ℂ на ℂ.

LaTeX

$$$ conjCLE : \\\\mathbb{C} \\\\simeq_{\\\\mathbb{R}} \\\\mathbb{C} \\\\text{ with } z \\\\mapsto \\\\overline{z}$$$

Lean4

/-- Continuous linear equiv version of the conj function, from `ℂ` to `ℂ`. -/
def conjCLE : ℂ ≃L[ℝ] ℂ :=
  conjLIE

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