English
There is a continuous linear equivalence between A and the product selfAdjoint(A) × skewAdjoint(A) given by x ↦ (selfAdjointPart x, skewAdjointPart x).
Русский
Существует непрерывное линейное эквивалентное отображение между A и произведением самосопряжённых и кососопряжённых частей: x ↦ (selfAdjointPart x, skewAdjointPart x).
LaTeX
$$$A \\cong_L[R] \\operatorname{selfAdjoint}(A) \\times \\operatorname{skewAdjoint}(A).$$$
Lean4
/-- The decomposition of elements of a star module into their self- and skew-adjoint parts,
as a continuous linear equivalence. -/
@[simps!]
def decomposeProdAdjointL [IsTopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] :
A ≃L[R] selfAdjoint A × skewAdjoint A
where
toLinearEquiv := StarModule.decomposeProdAdjoint R A
continuous_toFun := continuous_decomposeProdAdjoint _ _
continuous_invFun := continuous_decomposeProdAdjoint_symm _ _
