ne_zero_of_supDegree_ne_bot

Mathlib.Algebra.MonoidAlgebra.Degree

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

English

If the supremum degree of p with respect to D is not the bottom element, then p is nonzero.

Русский

Если p.supDegree D не равен ⊥, тогда p ≠ 0.

LaTeX

$$$p.supDegree D \neq \bot \Rightarrow p \neq 0$$$

Lean4

theorem ne_zero_of_supDegree_ne_bot : p.supDegree D ≠ ⊥ → p ≠ 0 :=
  mt (fun h => h ▸ supDegree_zero)

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

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

Разделы

Аффилиация

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