zero

Mathlib.Algebra.Star.SelfAdjoint

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

English

The element 1 is star-normal in any star-ring with star operation.

Русский

Единица является звездно-нормальной в любом кольце с операцией звезды.

LaTeX

$$$ [\\text{MulOneClass } R] [\\text{StarMul } R] \\Rightarrow IsStarNormal (1). $$$

Lean4

protected instance zero [NonUnitalNonAssocSemiring R] [StarAddMonoid R] : IsStarNormal (0 : R) :=
  ⟨by simp only [Commute.refl, star_zero]⟩

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

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

Разделы

Аффилиация

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