adjoint_inner_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- The fundamental property of the adjoint. -/
theorem adjoint_inner_right (A : E →ₗ[𝕜] F) (x : E) (y : F) : ⟪x, adjoint A y⟫ = ⟪A x, y⟫ :=
  by
  have := FiniteDimensional.complete 𝕜 E
  have := FiniteDimensional.complete 𝕜 F
  rw [← coe_toContinuousLinearMap A, adjoint_eq_toCLM_adjoint]
  exact ContinuousLinearMap.adjoint_inner_right _ x y

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