ne_zero_of_not_supDegree_le

Mathlib.Algebra.MonoidAlgebra.Degree

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.ne_zero_of_not_supDegree_le

English

If p.supDegree D is not bounded above by b, then p ≠ 0.

Русский

Если p.supDegree D не меньше или равно некоторому b, тогда p ≠ 0.

LaTeX

$$$\neg(p.supDegree D \le b) \Rightarrow p \neq 0$$$

Lean4

theorem ne_zero_of_not_supDegree_le {b : B} (h : ¬p.supDegree D ≤ b) : p ≠ 0 :=
  ne_zero_of_supDegree_ne_bot (fun he => h <| he ▸ bot_le)

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

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

Разделы

Аффилиация

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