Commit 2023-09-20 09:38 14b1439d

feat(NumberTheory.NumberField.CanonicalEmbedding): add exists_ne_zero_mem_ringOfIntegers_lt (#5650) This PR proves the following result:

theorem exists_ne_zero_mem_ringOfIntegers_lt (h : minkowski_bound K < volume (convex_body_lt K f)) :
     ∃ (a : 𝓞 K), a ≠ 0 ∧ ∀ w : InfinitePlace K, w a < f w 

where f : InfinitePlace K → ℝ≥0 and convex_body_lt K f is the set of points x such that ‖x w‖ < f w for all infinite places w. This is a key result in the proof of Dirichlet's unit theorem #5960