VectorAvoidance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A lattice vector off all coordinate hyperplanes

For a matrix with nonzero determinant, use the integer coefficient vector (1,N,...,N^(n-1)). Each coordinate of its row product is a nonzero polynomial in N. Finitely many polynomials exclude only finitely many integers, so a suitable integer N exists. This gives the vector selection used to deduce ordinary ball bounds from vector-box counts.

theorem OAI.DukePrimeDegree.exists_integer_row_all_ne_zero line 24
Source documentation
An invertible real matrix admits an integral row combination with no zero coordinate. No bound on the chosen coefficients is required.
```
theorem exists_integer_row_all_ne_zero {n : ℕ}
    (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.det ≠ 0) :
    ∃ c : Fin n → ℤ, ∀ j, (Matrix.vecMul (fun i => (c i : ℝ)) A) j ≠ 0 := by
…
```

theorem OAI.DukePrimeDegree.submodule_exists_all_coordinates_ne_zero line 60

Source documentation

Every additive integer lattice containing the rows of an invertible real matrix contains a vector with all coordinates nonzero.

theorem submodule_exists_all_coordinates_ne_zero {n : ℕ}
    (Λ : Submodule ℤ (Fin n → ℝ)) (A : Matrix (Fin n) (Fin n) ℝ)
    (hA : A.det ≠ 0) (hrows : ∀ i, A i ∈ Λ) :
    ∃ v ∈ Λ, ∀ j, v j ≠ 0 := by
…