exists_natDegree_lt — Mathlib

English

If p ∈ R[X] is monic of degree n with n > 0, then there exists q ∈ R[X] such that p = X^n + q and natDegree(q) < n.

Русский

Если полином p ∈ R[X] монический и имеет градус n > 0, то существует q ∈ R[X], такой что p = X^n + q и natDegree(q) < n.

LaTeX

$$$\exists q \in R[X],\; p = X^{n} + q \land \mathrm{natDegree}(q) < n$$$

Lean4

theorem exists_natDegree_lt {p : R[X]} {n : ℕ} (hn : n ≠ 0) (hp : IsMonicOfDegree p n) :
    ∃ q : R[X], p = X ^ n + q ∧ q.natDegree < n :=
  by
  refine ⟨p.eraseLead, ?_, ?_⟩
  · nth_rewrite 1 [← p.eraseLead_add_C_mul_X_pow]
    rw [add_comm, hp.natDegree_eq, hp.leadingCoeff_eq, map_one, one_mul]
  · refine p.eraseLead_natDegree_le.trans_lt ?_
    rw [hp.natDegree_eq]
    cutsat

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