Commit 2023-12-13 06:01 f7c6fc15
View on Github →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|