instStarModuleId

Mathlib.Analysis.InnerProductSpace.Adjoint

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

English

For endomorphisms A,B, the adjoint respects multiplication: (A ∘ B)† = B† ∘ A†.

Русский

Сопряжённый сохраняет порядок умножения: (A ∘ B)† = B† ∘ A†.

LaTeX

$$(A B)^{\dagger} = B^{\dagger} A^{\dagger}$$

Lean4

instance : StarModule 𝕜 (E →L[𝕜] E) :=
  ⟨LinearIsometryEquiv.map_smulₛₗ adjoint⟩

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

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

Разделы

Аффилиация

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