Siegel's Lemma #
In this file we introduce and prove Siegel's Lemma in its most basic version. This is a fundamental tool in diophantine approximation and transcendency and says that there exists a "small" integral non-zero solution of a non-trivial underdetermined system of linear equations with integer coefficients.
Main results #
exists_ne_zero_int_vec_norm_le
: Given a non-zerom × n
matrixA
withm < n
the linear system it determines has a non-zero integer solutiont
with‖t‖ ≤ ((n * ‖A‖) ^ ((m : ℝ) / (n - m)))
Notation #
‖_‖
: Matrix.seminormedAddCommGroup is the sup norm, the maximum of the absolute values of the entries of the matrix
References #
See [M. Hindry and J. Silverman, Diophantine Geometry: an Introduction][hindrysilverman00].