natDegree_sub_lt — Mathlib

English

If p and q are both monic of the same degree n with n ≠ 0, then p − q has natDegree strictly less than n.

Русский

Если p и q оба моноичны степени n (n ≠ 0), то p − q имеет natDegree строго меньшую, чем n.

LaTeX

$$$\\operatorname{natDegree}(p - q) < n$$$

Lean4

theorem natDegree_sub_lt {p q : R[X]} {n : ℕ} (hn : n ≠ 0) (hp : IsMonicOfDegree p n) (hq : IsMonicOfDegree q n) :
    (p - q).natDegree < n := by
  rw [← sub_sub_sub_cancel_right p q (X ^ n)]
  replace hp := hp.natDegree_sub_X_pow hn
  replace hq := hq.natDegree_sub_X_pow hn
  rw [← Nat.le_sub_one_iff_lt (Nat.zero_lt_of_ne_zero hn)] at hp hq ⊢
  exact (natDegree_sub_le_iff_left hq).mpr hp

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