natDegree_mod_lt — Mathlib

English

If q is nonzero, then the natDegree of p % q is less than natDegree q.

Русский

Если q ≠ 0, то natDegree(p % q) < natDegree(q).

LaTeX

$$$ (p \bmod q).\mathrm{natDegree} < q.\mathrm{natDegree} $$$

Lean4

theorem natDegree_mod_lt [Field k] (p : k[X]) {q : k[X]} (hq : q.natDegree ≠ 0) : (p % q).natDegree < q.natDegree :=
  by
  have hq' : q.leadingCoeff ≠ 0 := by
    rw [leadingCoeff_ne_zero]
    contrapose! hq
    simp [hq]
  rw [mod_def]
  refine (natDegree_modByMonic_lt p ?_ ?_).trans_le ?_
  · refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
    rw [mul_inv_eq_one₀ hq']
  · contrapose! hq
    rw [← natDegree_mul_C_eq_of_mul_eq_one ((inv_mul_eq_one₀ hq').mpr rfl)]
    simp [hq]
  · exact natDegree_mul_C_le q q.leadingCoeff⁻¹

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