clm_adjoint_eq — Mathlib

English

If A is a symmetric continuous linear map on a 𝕜-Hilbert space, then A is equal to its adjoint: A† = A.

Русский

Если A — симметричный непрерывно линейный оператор на гильбертовом пространстве над 𝕜, то A совпадает со своим сопряжённым: A† = A.

LaTeX

$$$A^{\dagger} = A$$$

Lean4

@[simp]
theorem _root_.LinearMap.IsSymmetric.clm_adjoint_eq {A : E →L[𝕜] E} (hA : A.IsSymmetric) : A† = A := by
  rwa [eq_comm, eq_adjoint_iff A A]

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