abs_discr_gt_two — Mathlib

English

A nontrivial number field has discriminant greater than 2; more precisely, |discr(K)| > 2 for any nontrivial K.

Русский

Неприводимое число поля имеет дискриминант больше 2; в частности, |discr(K)| > 2 для любого непустого поля.

LaTeX

$$$2 < |\mathrm{discr}(K)|$$$

Lean4

/-- **Hermite-Minkowski Theorem**. A nontrivial number field has discriminant greater than `2`. -/
theorem abs_discr_gt_two (h : 1 < finrank ℚ K) : 2 < |discr K| :=
  by
  rw [← Nat.succ_le_iff] at h
  rify
  calc
    (2 : ℝ) < (4 / 9) * (3 * π / 4) ^ 2 := by nlinarith [Real.pi_gt_three]
    _ ≤ (4 / 9 : ℝ) * (3 * π / 4) ^ finrank ℚ K := by
      gcongr
      linarith [Real.pi_gt_three]
    _ ≤ |(discr K : ℝ)| := mod_cast abs_discr_ge h

Похожие утверждения