bot_eq_zero

Mathlib.Data.Finsupp.MonomialOrder

URI: https://scilib.ai/kg/mathlib#MonomialOrder.bot_eq_zero

English

Every element of the domain is nonnegative under the MonomialOrder, i.e., 0 ≤ a for all a.

Русский

Каждый элемент домена неотрицателен относительно порядка мономов: 0 ≤ a для всех a.

LaTeX

$$$$ 0 \\le a. $$$$

Lean4

@[simp]
theorem bot_eq_zero : (⊥ : m.syn) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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