adjoint_inner_left — Mathlib

English

The inner product identity holds for adjoint: ⟪A† y, x⟫ = ⟪y, A x⟫.

Русский

Свойство внутреннего произведения остаётся верным для сопряжённого: ⟪A† y, x⟫ = ⟪y, A x⟫.

LaTeX

$$$$ \\langle A^{\\dagger} y, x \\rangle = \\langle y, A x \\rangle. $$$$

Lean4

/-- The fundamental property of the adjoint. -/
theorem adjoint_inner_left (A : E →L[𝕜] F) (x : E) (y : F) : ⟪(A†) y, x⟫ = ⟪y, A x⟫ :=
  adjointAux_inner_left A x y

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