degree_modByMonic_le

Mathlib.Algebra.Polynomial.Div

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

← MathLib Explorer

English

For monic q, deg(p %ₘ q) ≤ deg p.

Русский

Для монического q, deg(p %ₘ q) ≤ deg p.

LaTeX

$$$ \deg(p \%_{m} q) \leq \deg p \quad (\operatorname{Monic}(q)) $$$

Lean4

theorem degree_modByMonic_le (p : R[X]) {q : R[X]} (hq : Monic q) : degree (p %ₘ q) ≤ degree q :=
  by
  nontriviality R
  exact (degree_modByMonic_lt _ hq).le

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

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

Разделы

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

Аффилиация

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