natDegree_eq_of_natDegree_add_lt_right

Mathlib.Algebra.Polynomial.Degree.Operations

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

← MathLib Explorer

English

If natDegree(p+q) < natDegree(q), then natDegree(p) = natDegree(q).

Русский

Если natDegree(p+q) < natDegree(q), то natDegree(p) = natDegree(q).

LaTeX

$$$natDegree(p + q) < natDegree(q) \Rightarrow natDegree(p) = natDegree(q)$$$

Lean4

theorem natDegree_eq_of_natDegree_add_lt_right (p q : R[X]) (H : natDegree (p + q) < natDegree q) :
    natDegree p = natDegree q :=
  (natDegree_eq_of_natDegree_add_lt_left q p (add_comm p q ▸ H)).symm

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

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

Разделы

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

Аффилиация

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