instIsStarNormal — Mathlib

English

Every unitary element u is IsStarNormal, i.e., star(u) commutes with u in the sense of the normality condition.

Русский

Каждый унитарный элемент u удовлетворяет условию IsStarNormal, то есть звезда(u) коммутирует с u в смысле нормальности.

LaTeX

$$$ \forall u \in \mathrm{unitary}(R),\; \mathrm{IsStarNormal}(u) $$$

Lean4

instance instIsStarNormal (u : unitary R) : IsStarNormal u where
  star_comm_self := star_mul_self u |>.trans <| (mul_star_self u).symm

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