degree_gcd_le_right

Mathlib.RingTheory.Polynomial.Content

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

English

Symmetrically, deg(gcd(p,q)) ≤ deg(q) when q ≠ 0.

Русский

Аналогично, deg(gcd(p,q)) ≤ deg(q) при q ≠ 0.

LaTeX

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

Lean4

theorem degree_gcd_le_right (p) {q : R[X]} (hq : q ≠ 0) : (gcd p q).degree ≤ q.degree :=
  by
  rw [gcd_comm]
  exact degree_gcd_le_left hq p

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

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

Разделы

Аффилиация

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