star_comm_self'

Mathlib.Algebra.Star.SelfAdjoint

URI: https://scilib.ai/kg/mathlib#star_comm_self'

English

If x is star-normal, then star x commutes with x: star x · x = x · star x.

Русский

Если x звездо-нормален, то он коммуницирует со своей звездой: star x · x = x · star x.

LaTeX

$$$\\\\star x \\\\cdot x = x \\\\cdot \\\\star x.$$$

Lean4

theorem star_comm_self' [Mul R] [Star R] (x : R) [IsStarNormal x] : star x * x = x * star x :=
  IsStarNormal.star_comm_self

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

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

Разделы

Аффилиация

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