eq_zero_iff

Mathlib.Data.Finsupp.MonomialOrder

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

English

An element a of the exponent space is mapped to 0 by the underlying synorphism if and only if a is zero.

Русский

Элемент экспонентного пространства отображается в 0 под основу синхрализованного отображения тогда и только тогда, когда a = 0.

LaTeX

$$$$ m.toSyn(a) = 0 \\iff a = 0. $$$$

Lean4

theorem eq_zero_iff {a : m.syn} : a = 0 ↔ a ≤ 0 :=
  eq_bot_iff

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

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

Разделы

Аффилиация

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