toSyn_lt_iff_ne_zero

Mathlib.Data.Finsupp.MonomialOrder

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

English

Let m be a Monomial Order on σ. For every a in the substructure m.syn, we have 0 < a if and only if a ≠ 0.

Русский

Пусть m задаёт порядок мономов на σ. Для каждого элемента a из m.syn выполняется 0 < a тогда и только тогда, когда a ≠ 0.

LaTeX

$$$0 < a \iff a \neq 0$$$

Lean4

theorem toSyn_lt_iff_ne_zero {a : m.syn} : 0 < a ↔ a ≠ 0 :=
  bot_lt_iff_ne_bot

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

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

Разделы

Аффилиация

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