ne_zero_of_natDegree_gt

Mathlib.Algebra.Polynomial.Degree.Operations

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

English

If n < natDegree p, then p ≠ 0.

Русский

Если n < natDegree p, то p ≠ 0.

LaTeX

$$$ p \in R[X],\; n < \operatorname{natDegree}(p) \Rightarrow p \neq 0 $$$

Lean4

theorem ne_zero_of_natDegree_gt {n : ℕ} (h : n < natDegree p) : p ≠ 0 := fun H => by simp [H] at h

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

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

Разделы

Аффилиация

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