adjoint — Mathlib

English

The adjoint is involutive: (A^*)^* = A for a linear map A.

Русский

Сопряжённое оператора: (A^*)^* = A.

LaTeX

$$$\\text{adjoint}(\\text{adjoint}(A)) = A$$$

Lean4

/-- The adjoint of an operator from the finite-dimensional inner product space `E` to the
finite-dimensional inner product space `F`. -/
def adjoint : (E →ₗ[𝕜] F) ≃ₗ⋆[𝕜] F →ₗ[𝕜] E :=
  haveI := FiniteDimensional.complete 𝕜 E
  haveI := FiniteDimensional.complete 𝕜 F
  ((LinearMap.toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F).trans
        ContinuousLinearMap.adjoint.toLinearEquiv).trans
    LinearMap.toContinuousLinearMap.symm

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