English
There is a natural real-linear identification between self-adjoint elements of the complex numbers and the real line, given by taking real parts. Concretely, z in self-adjoint(ℂ) corresponds to Re(z) in ℝ, and the inverse sends x in ℝ to the complex number with real part x and imaginary part 0.
Русский
Существует естественное ℝ–линейное соответствие между самосопряжёнными элементами ℂ и ℝ, задаваемое взятием вещественной части. Конкретно: z ∈ selfAdjoint(ℂ) соответствует Re(z) ∈ ℝ, а обратное отображение отправляет x ∈ ℝ в комплексное число с вещественной частью x и нулевой мнимой частью.
LaTeX
$$$\mathrm{SelfAdjoint}(\mathbb{C}) \cong_{\mathbb{R}} \mathbb{R}$, \\ z \mapsto \Re(z), \quad x \mapsto x \text{ (as an element of } \mathbb{C}\text{).}$$$
Lean4
/-- The natural `ℝ`-linear equivalence between `selfAdjoint ℂ` and `ℝ`. -/
@[simps apply symm_apply]
def selfAdjointEquiv : selfAdjoint ℂ ≃ₗ[ℝ] ℝ
where
toFun := fun z ↦ (z : ℂ).re
invFun := fun x ↦ ⟨x, conj_ofReal x⟩
left_inv := fun z ↦ Subtype.ext <| conj_eq_iff_re.mp z.property.star_eq
map_add' := by simp
map_smul' := by simp
