adjoint_toContinuousLinearMap — Mathlib

English

The fundamental property: ⟪adjoint A y, x⟫ = ⟪y, A x⟫.

Русский

Основное свойство: ⟪A^* y, x⟫ = ⟪y, A x⟫.

LaTeX

$$$\\langle \\operatorname{adjoint} A\, y, x \\rangle = \\langle y, A x \\rangle$$$

Lean4

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

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