adjoint_eq

Mathlib.Analysis.InnerProductSpace.Adjoint

URI: https://scilib.ai/kg/mathlib#LinearMap.IsSymmetric.adjoint_eq

English

If A is symmetric (self-adjoint) then A equals its adjoint: A† = A.

Русский

Если A симметричен (самосопряжённый), то A равно своему сопряжению: A† = A.

LaTeX

$$$$A^{*} = A \quad\text{whenever } A \text{ is symmetric}$$$$

Lean4

@[simp]
theorem adjoint_eq {A : E →ₗ[𝕜] E} (hA : A.IsSymmetric) : A.adjoint = A := by rwa [eq_comm, eq_adjoint_iff A A]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru