toSyn_eq_zero_iff

Mathlib.Data.Finsupp.MonomialOrder

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

English

Equivalently, the embedding toSyn is zero-preserving and injective on the zero element.

Русский

Эквивалентно: отображение toSyn сохраняет нуль и инъективно на нуль.

LaTeX

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

Lean4

theorem toSyn_eq_zero_iff (a : σ →₀ ℕ) : m.toSyn a = 0 ↔ a = 0 :=
  AddEquiv.map_eq_zero_iff m.toSyn

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

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

Разделы

Аффилиация

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