English
The imaginary part map is defined as the negative I times the skew-adjoint part after projecting onto the real part, giving a linear map from A to self-adjoint elements.
Русский
Мнимая часть определяется как отрицательное i, умноженное на претактированную на действительную часть косо-сопряжённую часть, образующее линейное отображение в selfAdjoint.
LaTeX
$$$\\text{imaginaryPart} = \\big( -\\mathrm{i} \\big) \\cdot \\big( \\text{skewAdjointPart} \\big) \\circ \\text{skewAdjointPartReal}$$$
Lean4
/-- The imaginary part `ℑ a` of an element `a` of a star module over `ℂ`, as a linear map into the
self adjoint elements. In a general star module, we have a decomposition into the `selfAdjoint`
and `skewAdjoint` parts, but in a star module over `ℂ` we have
`realPart_add_I_smul_imaginaryPart`, which allows us to decompose into a linear combination of
`selfAdjoint`s. -/
noncomputable def imaginaryPart : A →ₗ[ℝ] selfAdjoint A :=
skewAdjoint.negISMul.comp (skewAdjointPart ℝ)
