adjoint_adjoint

Mathlib.Analysis.InnerProductSpace.Adjoint

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.adjoint_adjoint

English

The adjoint of the adjointAux map equals the original map: adjointAux (adjointAux A) = A.

Русский

Сопряжённость двухступенчатого оператора равна исходному: adjointAux (adjointAux A) = A.

LaTeX

$$$$ \\mathrm{adjointAux}( \\mathrm{adjointAux} A ) = A. $$$$

Lean4

/-- The adjoint is involutive. -/
@[simp]
theorem adjoint_adjoint (A : E →L[𝕜] F) : A†† = A :=
  adjointAux_adjointAux A

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

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

Разделы

Аффилиация

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