isSelfAdjoint_inner_self

Mathlib.Analysis.CStarAlgebra.Module.Defs

URI: https://scilib.ai/kg/mathlib#CStarModule.isSelfAdjoint_inner_self

English

For any x in E, the element ⟪x,x⟫ is self-adjoint in A: IsSelfAdjoint ⟪x,x⟫.

Русский

Для любого x в E элемент ⟪x, x⟫ самоприводим к сопряжённому: IsSelfAdjoint ⟪x,x⟫.

LaTeX

$$$IsSelfAdjoint\\\\langle x, x \\\\rangle_A$$$

Lean4

@[simp]
theorem isSelfAdjoint_inner_self {x : E} : IsSelfAdjoint ⟪x, x⟫ :=
  star_inner _ _

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

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

Разделы

Аффилиация

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