skewAdjointPartL — Mathlib

English

The skew-adjoint part map is a continuous linear map from A to the skew-adjoint part of A.

Русский

Отображение на кососопряжённую часть является непрерывным линейным отображением из A в кососопряжённую часть A.

LaTeX

$$$S: A \\to_L[R] \\operatorname{skewAdjoint}(A),\\quad S(x)=\\operatorname{skewAdjointPart}(x).$$$

Lean4

/-- The skew-adjoint part of an element of a star module, as a continuous linear map. -/
@[simps!]
def skewAdjointPartL [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A] : A →L[R] skewAdjoint A
    where
  toLinearMap := skewAdjointPart R
  cont := continuous_skewAdjointPart _ _

Похожие утверждения