English
The real part map is the canonical projection onto the self-adjoint part of A, i.e., a linear map sending each element to its self-adjoint component.
Русский
Действительная часть — это канонический проекционный отображение на самосопряженную часть A.
LaTeX
$$$\\operatorname{realPart} : A \\to \\operatorname{selfAdjoint} A\\quad( a \\mapsto \\text{selfAdjoint part of } a )$$$
Lean4
/-- The real part `ℜ a` of an element `a` of a star module over `ℂ`, as a linear map. This is just
`selfAdjointPart ℝ`, but we provide it as a separate definition in order to link it with lemmas
concerning the `imaginaryPart`, which doesn't exist in star modules over other rings. -/
noncomputable def realPart : A →ₗ[ℝ] selfAdjoint A :=
selfAdjointPart ℝ
