natDegree_sub_X_pow — Mathlib

English

Let p be a monic polynomial of degree n over a ring R with n ≠ 0. Then the natDegree of p − X^n is strictly less than n.

Русский

Пусть p — моноический многочлен над кольцом R степени n, причём n ≠ 0. Тогда natDegree(p − X^n) строго меньше n.

LaTeX

$$$\\operatorname{natDegree}\\bigl(p - X^n\\bigr) < n$$$

Lean4

theorem natDegree_sub_X_pow {p : R[X]} {n : ℕ} (hn : n ≠ 0) (hp : IsMonicOfDegree p n) : (p - X ^ n).natDegree < n :=
  by
  obtain ⟨q, hq₁, hq₂⟩ := hp.exists_natDegree_lt hn
  simpa [hq₁]

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