Relations among a finite family of algebra-valued polynomials can be encoded by a finite scalar polynomial matrix. Persistent dependence therefore gives a polynomial relation nonzero at the origin, even when the target algebra is infinite-dimensional over the scalar field.

Apply a linear functional to the coefficients of a univariate polynomial. This commutes with evaluation over the scalar field and multiplication by scalar polynomials, allowing polynomial relations to be encoded by matrices.

theorem CCDN.polynomial_family_relation_nonzero_at_zero {K : Type u_1} {A : Type u_2} {κ : Type u_3} [Field K] [CharZero K] [CommRing A] [Algebra K A] [Fintype κ] (g : κ → Polynomial A) (hdep : ∀ (k : ℕ), ∃ (c : κ → K), c ≠ 0 ∧ ∑ j : κ, c j • Polynomial.eval (↑k) (g j) = 0) : ∃ (v : κ → Polynomial K), ∑ j : κ, Polynomial.map (algebraMap K A) (v j) * g j = 0 ∧ ∃ (j : κ), Polynomial.eval 0 (v j) ≠ 0

If the evaluations of a polynomial family are dependent over K at every integer parameter, the family has a polynomial relation whose coefficient vector does not vanish at zero.