English
The real part restricted to the self-adjoint submodule is the identity map.
Русский
Пределение действительной части на подпространстве самосопряжённых элементов является тождественным отображением.
LaTeX
$$$\\text{realPart} \\circ (\\text{selfAdjoint.submodule } \\mathbb{R} \\; A)\\;\\text{subtype} = \\mathrm{id}$$$
Lean4
@[scoped macro ComplexStarModule.termℑ]
public meta def _aux_Mathlib_LinearAlgebra_Complex_Module___macroRules_ComplexStarModule_termℑ_1 : Macro✝ := fun
| `(ℑ) => ``(imaginaryPart)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
