English
Let A : E →L[𝕜] F and B : F →L[𝕜] E be bounded linear maps between complex inner product spaces. Then A is the adjoint of B if and only if for every x ∈ E and y ∈ F we have ⟪A x, y⟫ = ⟪x, B y⟫.
Русский
Пусть A : E →L[𝕜] F и B : F →L[𝕜] E — ограниченные линейные отображения между комплексными пространствами с вложенным скалярным произведением. Тогда A является сопряженным к B тогда и только тогда, когда для всех x ∈ E и y ∈ F выполняется ⟪A x, y⟫ = ⟪x, B y⟫.
LaTeX
$$$A = B^{\dagger} \iff \forall x \in E, \forall y \in F: \langle A x, y \rangle = \langle x, B y \rangle$$$
Lean4
/-- The adjoint is unique: a map `A` is the adjoint of `B` iff it satisfies `⟪A x, y⟫ = ⟪x, B y⟫`
for all `x` and `y`. -/
theorem eq_adjoint_iff (A : E →L[𝕜] F) (B : F →L[𝕜] E) : A = B† ↔ ∀ x y, ⟪A x, y⟫ = ⟪x, B y⟫ :=
by
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
ext x
exact ext_inner_right 𝕜 fun y => by simp only [adjoint_inner_left, h x y]
