isStarNormal

Mathlib.Algebra.Star.StarProjection

URI: https://scilib.ai/kg/mathlib#IsStarProjection.isStarNormal

English

If p is a star projection, then it is normal: p p^* = p^* p.

Русский

Если p — звездная проекция, то она нормальна: p p^* = p^* p.

LaTeX

$$$ p p^* = p^* p $$$

Lean4

theorem isStarNormal [Mul R] [Star R] (hp : IsStarProjection p) : IsStarNormal p :=
  hp.isSelfAdjoint.isStarNormal

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

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

Разделы

Аффилиация

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