degree_ne_bot

Mathlib.Algebra.Polynomial.Degree.Definitions

URI: https://scilib.ai/kg/mathlib#Polynomial.degree_ne_bot

English

degree p ≠ ⊥ is equivalent to p ≠ 0.

Русский

degree p ≠ ⊥ эквивалентно p ≠ 0.

LaTeX

$$$\deg(p) \neq \bot \iff p \neq 0$$$

Lean4

theorem degree_ne_bot : degree p ≠ ⊥ ↔ p ≠ 0 :=
  degree_eq_bot.not

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

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

Разделы

Аффилиация

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