ne_zero_of_coe_le_degree

Mathlib.Algebra.Polynomial.Degree.SmallDegree

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

English

Let n ∈ ℕ and p ∈ R[X]. If ↑n ≤ degree(p), then p ≠ 0.

Русский

Пусть n ∈ ℕ и p ∈ R[X]. Если ↑n ≤ deg(p), то p ≠ 0.

LaTeX

$$$(\uparrow n \le p.degree) \Rightarrow p \neq 0$$$

Lean4

theorem ne_zero_of_coe_le_degree (hdeg : ↑n ≤ p.degree) : p ≠ 0 :=
  zero_le_degree_iff.mp <| (WithBot.coe_le_coe.mpr n.zero_le).trans hdeg

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

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

Разделы

Аффилиация

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