zero

Mathlib.Algebra.Star.StarProjection

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

English

The zero element is a star projection: 0^2 = 0 and 0^* = 0.

Русский

Нуль является звездной проекцией: 0^2 = 0 и 0^* = 0.

LaTeX

$$$ 0^2 = 0 \land 0^* = 0 $$$

Lean4

@[simp]
protected theorem zero [NonUnitalNonAssocSemiring R] [StarAddMonoid R] : IsStarProjection (0 : R) :=
  ⟨.zero, .zero _⟩

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

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

Разделы

Аффилиация

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