Commit 2023-12-13 06:01 f7c6fc15

feat: Hermite-Minkowski theorem (#8478) We prove lower bounds for the abs. value of the discriminant of a number field in terms of its degree and deduce from it Hermite-Minkowski theorem: a nontrivial number field has nontrivial absolute discriminant.

theorem abs_discr_ge (h : 1 < finrank ℚ K) :
    (4 / 9 : ℝ) * (3 * π / 4) ^ finrank ℚ K ≤ |discr K| 
theorem discr_gt_one (h : 1 < finrank ℚ K) : 2 < |discr K|