A polynomial matrix with dependent columns at every integer value has a polynomial kernel vector that remains nonzero at zero. A common power of X is removed from a kernel vector after its rational denominators are cleared.

theorem CCDN.polynomial_matrix_kernel_nonzero_at_zero {K : Type u_1} {ι : Type u_2} {κ : Type u_3} [Field K] [CharZero K] [Finite ι] [Fintype κ] (A : Matrix ι κ (Polynomial K)) (hA : ∀ (k : ℕ), ¬Function.Injective ⇑(A.map ⇑(Polynomial.evalRingHom ↑k)).mulVecLin) : ∃ (v : κ → Polynomial K), A.mulVec v = 0 ∧ ∃ (j : κ), Polynomial.eval 0 (v j) ≠ 0

If every integer specialization has dependent columns, there is a polynomial relation whose constant coefficient vector is nonzero.