Polynomial det nat Degree le sum

import Mathlib.Algebra.Polynomial.Div
import Mathlib.LinearAlgebra.Matrix.Polynomial

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_det_natDegree_le_sum (P : Matrix ι ι R[X]) (d : ι → ℕ)
    (hdeg : ∀ i j, (P i j).natDegree ≤ d j) :
    P.det.natDegree ≤ ∑ j, d j := by sorry







end CommRing

end D1Bound5
end