Theorem Int.Matrix.exists_ne_zero_int_vec_norm_le

Modification history

2024-08-09 00:58
Mathlib/NumberTheory/SiegelsLemma.lean
chore: backports for leanprover/lean4#4814 (part 24) (#15520)
Modified Int.Matrix.exists_ne_zero_int_vec_norm_leView on Github →
2024-07-19 17:33
Mathlib/NumberTheory/SiegelsLemma.lean
feat: generalize Siegel's lemma to `A = 0` (#14852) …
Modified Int.Matrix.exists_ne_zero_int_vec_norm_leView on Github →
2024-07-16 12:01
Mathlib/NumberTheory/SiegelsLemma.lean
feat(NumberTheory/SiegelsLemma): replace `Fin m` and `Fin n` with `Fintype α` and `Fintype β` (#14797)
Modified Int.Matrix.exists_ne_zero_int_vec_norm_leView on Github →
2024-06-22 09:09
Mathlib/NumberTheory/SiegelsLemma.lean
feat(NumberTheory/SiegelsLemma): Siegel's lemma for small integral non-trivial solutions of linear systems (#13487) …
Added Int.Matrix.exists_ne_zero_int_vec_norm_leView on Github →