adjointAux_adjointAux — Mathlib

English

Fundamental inner product identity 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

theorem adjointAux_adjointAux (A : E →L[𝕜] F) : adjointAux (adjointAux A) = A :=
  by
  ext v
  refine ext_inner_left 𝕜 fun w => ?_
  rw [adjointAux_inner_right, adjointAux_inner_left]

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