degree_gcd_le_left

Mathlib.RingTheory.Polynomial.Content

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

← MathLib Explorer

English

If p ≠ 0, then for any q, deg(gcd(p,q)) ≤ deg(p).

Русский

Если p ≠ 0, то для любого q deg(gcd(p,q)) ≤ deg(p).

LaTeX

$$$p \neq 0 \Rightarrow \deg(\gcd(p,q)) \le \deg(p)$$$

Lean4

theorem degree_gcd_le_left {p : R[X]} (hp : p ≠ 0) (q) : (gcd p q).degree ≤ p.degree :=
  by
  have := natDegree_le_iff_degree_le.mp (natDegree_le_of_dvd (gcd_dvd_left p q) hp)
  rwa [degree_eq_natDegree hp]

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

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

Разделы

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

Аффилиация

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