isSelfAdjoint — Mathlib

English

If the underlying linear map of A is symmetric, then A is self-adjoint.

Русский

Если соответствующая линейная карта A симметрична, то A является самосопряжённой.

LaTeX

$$$\\text{If } (A : E \\to E) \\text{ IsSymmetric, then } IsSelfAdjoint(A)$$$

Lean4

theorem _root_.LinearMap.IsSymmetric.isSelfAdjoint {A : E →L[𝕜] E} (hA : (A : E →ₗ[𝕜] E).IsSymmetric) :
    IsSelfAdjoint A := by rwa [← ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric] at hA

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