natDegree_le_natDegree

Mathlib.Algebra.Polynomial.Degree.Definitions

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

← MathLib Explorer

English

If deg p ≤ deg q for polynomials p ∈ R[X], q ∈ S[X], then natDegree p ≤ natDegree q.

Русский

Если deg p ≤ deg q для полиномов p ∈ R[X], q ∈ S[X], тогда natDegree p ≤ natDegree q.

LaTeX

$$p.degree ≤ q.degree \\Rightarrow p.natDegree ≤ q.natDegree$$

Lean4

theorem natDegree_le_natDegree [Semiring S] {q : S[X]} (hpq : p.degree ≤ q.degree) : p.natDegree ≤ q.natDegree :=
  WithBot.giUnbotDBot.gc.monotone_l hpq

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

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

Разделы

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

Аффилиация

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