natDegree_modByMonic_lt — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem natDegree_modByMonic_lt (p : R[X]) {q : R[X]} (hmq : Monic q) (hq : q ≠ 1) : natDegree (p %ₘ q) < q.natDegree :=
  by
  by_cases hpq : p %ₘ q = 0
  · rw [hpq, natDegree_zero, Nat.pos_iff_ne_zero]
    contrapose! hq
    exact eq_one_of_monic_natDegree_zero hmq hq
  · haveI := Nontrivial.of_polynomial_ne hpq
    exact natDegree_lt_natDegree hpq (degree_modByMonic_lt p hmq)

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