English
Let A: E → F and B: F → E be linear maps. Then A equals the adjoint of B if and only if for all x in E and y in F, ⟪A x, y⟫ = ⟪x, B y⟫.
Русский
Пусть A: E → F и B: F → E — линейные отображения. Тогда A равно сопряжению B тогда и только тогда, когда для всех x ∈ E, y ∈ F верно ⟪A x, y⟫ = ⟪x, B y⟫.
LaTeX
$$$$A = B^{*} \;\;\Leftrightarrow\;\; \forall x\in E, \forall y\in F, \langle Ax, y\rangle = \langle x, By\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 →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) : A = B.adjoint ↔ ∀ 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]
