natDegree_le_of_dvd

Mathlib.Algebra.Polynomial.Degree.Domain

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

← MathLib Explorer

English

If p ∣ q and q ≠ 0, then degree p ≤ degree q.

Русский

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

LaTeX

$$degree(p) ≤ degree(q)$$

Lean4

theorem natDegree_le_of_dvd (h1 : p ∣ q) (h2 : q ≠ 0) : p.natDegree ≤ q.natDegree :=
  by
  obtain ⟨q, rfl⟩ := h1
  rw [mul_ne_zero_iff] at h2
  rw [natDegree_mul h2.1 h2.2]; exact Nat.le_add_right _ _

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

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

Разделы

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

Аффилиация

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