isSelfAdjoint_iff'

Mathlib.Analysis.InnerProductSpace.Adjoint

URI: https://scilib.ai/kg/mathlib#LinearMap.isSelfAdjoint_iff'

← MathLib Explorer

English

The adjoint of the identity map is the identity map.

Русский

Сопряжение тождества — тождественное отображение.

LaTeX

$$$$(\mathrm{id})^{*} = \mathrm{id}.$$$$

Lean4

/-- A continuous linear operator is self-adjoint iff it is equal to its adjoint. -/
theorem isSelfAdjoint_iff' {A : E →ₗ[𝕜] E} : IsSelfAdjoint A ↔ A.adjoint = A :=
  Iff.rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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