degree_div_le

Mathlib.Algebra.Polynomial.FieldDivision

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

← MathLib Explorer

English

For any polynomials p and q, deg(p/q) ≤ deg p (provided q ≠ 0).

Русский

Для любых многочленов p и q выполняется deg(p/q) ≤ deg p (при q ≠ 0).

LaTeX

$$$ \deg\left(\frac{p}{q}\right) \le \deg p $$$

Lean4

theorem degree_div_le (p q : R[X]) : degree (p / q) ≤ degree p :=
  by
  by_cases hq : q = 0
  · simp [hq]
  · rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq]; exact degree_divByMonic_le _ _

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

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

Разделы

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

Аффилиация

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