degree_modByMonic_le_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem degree_modByMonic_le_left : degree (p %ₘ q) ≤ degree p :=
  by
  nontriviality R
  by_cases hq : q.Monic
  · cases lt_or_ge (degree p) (degree q)
    · rw [(modByMonic_eq_self_iff hq).mpr ‹_›]
    · exact (degree_modByMonic_le p hq).trans ‹_›
  · rw [modByMonic_eq_of_not_monic p hq]

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