instIdemCommSemiring

Mathlib.Algebra.Order.Kleene

URI: https://scilib.ai/kg/mathlib#Prod.instIdemCommSemiring

English

For any a, a ≤ a* (alternative form).

Русский

Для любого a выполняется a ≤ a* (альтернативная форма).

LaTeX

$$$\forall a \in \alpha,\ a \le a^*$$$

Lean4

instance [IdemCommSemiring α] [IdemCommSemiring β] : IdemCommSemiring (α × β) :=
  { Prod.instCommSemiring, Prod.instIdemSemiring with }

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

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

Разделы

Аффилиация

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