Commit 2024-06-22 09:09 ab0de47a
View on Github →feat(NumberTheory/SiegelsLemma): Siegel's lemma for small integral non-trivial solutions of linear systems (#13487)
This PR contains the proof of Siegel's Lemma.
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.
theorem exists_ne_zero_int_vec_norm_le: Given a non-singular m × n matrix A with m < n the linear
system it determines has a non-zero integer solution t with
‖t‖ ≤ ((n * ‖A‖) ^ ((m : ℝ) / (n - m)))
Zulip thread