15.4. The discriminant
The (absolute) discriminant of a number field is NumberField.discr, an integer computed from
an integral basis of 𝓞 K:
#check (NumberField.discr K : ℤ)
It is never zero, NumberField.discr_ne_zero:
example : discr K ≠ 0 := discr_ne_zero K
Two theorems connect the discriminant to the other invariants on this page.
The Hermite–Minkowski bound NumberField.abs_discr_gt_two states that any number
field other than ℚ has |discr K| > 2.
The Minkowski bound
NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr produces, in every
ideal class, an ideal whose norm is bounded in terms of √|discr K|; this is exactly the
input that makes the class group finite.