adjoint_eq_toCLM_adjoint — Mathlib

English

The adjoint is an involutive operator on linear maps: the adjoint of the adjoint is the original map.

Русский

Сопряжённое второго порядка возвращает исходное отображение.

LaTeX

$$$A^{\\*\\,*} = A$$$

Lean4

theorem adjoint_eq_toCLM_adjoint (A : E →ₗ[𝕜] F) :
    haveI := FiniteDimensional.complete 𝕜 E
    haveI := FiniteDimensional.complete 𝕜 F
    A.adjoint = A.toContinuousLinearMap.adjoint :=
  rfl

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