instCStarRingId

Mathlib.Analysis.InnerProductSpace.Adjoint

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

← MathLib Explorer

English

The operator norm satisfies ||A† A|| = ||A||^2.

Русский

Норма оператора удовлетворяет ||A† A|| = ||A||^2.

LaTeX

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

Lean4

/-- The C⋆-algebra instance when `𝕜 := ℂ` can be found in
`Mathlib/Analysis/CStarAlgebra/ContinuousLinearMap.lean`. -/
instance : CStarRing (E →L[𝕜] E) where norm_mul_self_le x := le_of_eq <| Eq.symm <| norm_adjoint_comp_self x

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

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

Разделы

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

Аффилиация

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