Commit 2023-11-03 16:13 2e15c5a0

feat: use Minkowski's theorem to prove the existence of algebraic integers of small norm (#8128) We define the convex body convexBodySum and prove the following

theorem exists_ne_zero_mem_ringOfIntegers_of_norm_le {B : ℝ}
     (h : (minkowskiBound K) < volume (convexBodySum K B)) :
     ∃ (a : 𝓞 K), a ≠ 0 ∧ |Algebra.norm ℚ (a:K)| ≤ ((finrank ℚ K : ℝ)⁻¹ * B) ^ (finrank ℚ K) 

Computation of the volume (convexBodySum K B)) and applications of the result are coming in a following PR.