Independent rows can be selected from the finite evaluation matrix. A nonzero annihilator gives the strict rank deficiency required by Bombieri--Vaaler.

The determinant argument selects independent evaluation rows. This module justifies why a coefficient vector annihilating those rows vanishes on every point whose row they span.

theorem CCDN.vanishes_of_evaluation_row_mem_span {n N s : ℕ} (mon : Fin N → Fin n →₀ ℕ) (points : Fin s → Fin n → ℤ) (v : Fin N → ℤ) (hAv : (evaluationMatrix mon points).mulVec v = 0) (x : Fin n → ℤ) (hx : (fun (j : Fin N) => ↑((mon j).prod fun (k : Fin n) (e : ℕ) => x k ^ e)) ∈ Submodule.span ℚ (Set.range ((evaluationMatrix mon points).map Int.cast).row)) : (MvPolynomial.eval x) (polynomialOfCoefficients mon v) = 0

If an integer coefficient vector v annihilates the evaluation matrix of the monomials mon at the points points, then the polynomial with coefficients v vanishes at every integer point x whose monomial evaluation row lies in the ℚ-span of the matrix rows.

theorem CCDN.exists_independent_spanning_rows {F : Type u_1} {ι : Type u_2} [Field F] {N : ℕ} (A : Matrix ι (Fin N) F) : ∃ (s : ℕ) (a : Fin s → ι), Function.Injective a ∧ LinearIndependent F (A.submatrix a id).row ∧ Submodule.span F (Set.range (A.submatrix a id).row) = Submodule.span F (Set.range A.row) ∧ s ≤ N

Every matrix with N columns has an injectively indexed family of s ≤ N linearly independent rows spanning its row space.

theorem CCDN.exists_independent_spanning_rows_lt {t N : ℕ} (A : Matrix (Fin t) (Fin N) ℚ) (v : Fin N → ℚ) (hv : v ≠ 0) (hker : A.mulVec v = 0) : ∃ (s : ℕ) (a : Fin s → Fin t), Function.Injective a ∧ LinearIndependent ℚ (A.submatrix a id).row ∧ Submodule.span ℚ (Set.range (A.submatrix a id).row) = Submodule.span ℚ (Set.range A.row) ∧ s < N

If a rational matrix with N columns has a nonzero kernel vector, then some injectively indexed family of s < N linearly independent rows spans its row space.