star

Mathlib.Algebra.Star.SelfAdjoint

URI: https://scilib.ai/kg/mathlib#IsStarNormal.star

← MathLib Explorer

English

If x is star-normal, then its star is also star-normal.

Русский

Если x звездо-нормален, то star x также нормален по звезде.

LaTeX

$$$ \\forall x \\in R, \\; [IsStarNormal x] \\Rightarrow IsStarNormal (\\star x). $$$

Lean4

protected instance star [Mul R] [StarMul R] {x : R} [IsStarNormal x] : IsStarNormal (star x) :=
  ⟨show star (star x) * star x = star x * star (star x) by rw [star_star, star_comm_self']⟩

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

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

Разделы

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

Аффилиация

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