ne_zero_of_degree_ge_degree

Mathlib.Algebra.Polynomial.Degree.Operations

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

← MathLib Explorer

English

If deg p ≤ deg q and p ≠ 0, then q ≠ 0.

Русский

Если deg p ≤ deg q и p ≠ 0, то q ≠ 0.

LaTeX

$$$ p, q \in R[X],\; p.degree \le q.degree \land p \neq 0 \Rightarrow q \neq 0 $$$

Lean4

theorem ne_zero_of_degree_ge_degree (hpq : p.degree ≤ q.degree) (hp : p ≠ 0) : q ≠ 0 :=
  Polynomial.ne_zero_of_degree_gt
    (lt_of_lt_of_le (bot_lt_iff_ne_bot.mpr (by rwa [Ne, Polynomial.degree_eq_bot])) hpq : q.degree > ⊥)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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