Polynomial eq top monomial of X pow dvd
ProvedD1Bound5.polynomial_eq_top_monomial_of_X_pow_dvddiophantine-tuplesnumber-theory
A polynomial whose degree is at most D and whose first D coefficients vanish is exactly its degree-D monomial, including the zero-polynomial case.
Preamble
import Mathlib.Algebra.Polynomial.Div import Mathlib.LinearAlgebra.Matrix.Polynomial
Formal statement
section
open Finset Polynomial Matrix
namespace D1Bound5
/-!
This module isolates an intermediate step in the all-orders Bennett determinant
argument. It does not define the residue polynomials or prove their cancellation.
The required cancellation is an explicit hypothesis of the final theorem.
-/
section CommRing
variable {R ι : Type*} [CommRing R] [Fintype ι] [DecidableEq ι]
theorem _root_.D1Bound5.polynomial_eq_top_monomial_of_X_pow_dvd (p : R[X]) (D : ℕ)
(hdeg : p.natDegree ≤ D) (hdiv : (X : R[X]) ^ D ∣ p) :
p = C (p.coeff D) * X ^ D := by sorry
end CommRing
end D1Bound5
end
Source
D1Bound5/BennettResidualDeterminant.lean, lines 50-64, SHA-256 d4ad136bba1428279a794309f2af79d21c79a906eda481e0c4808281896bf444. Project: https://github.com/tomislav-math/d1-bound5-lean