# Number field discriminant #

This file defines the discriminant of a number field.

## Tags #

number field, discriminant

@[reducible, inline]
noncomputable abbrev NumberField.discr (K : Type u_1) [] [] :

The absolute discriminant of a number field.

Equations
Instances For
theorem NumberField.coe_discr (K : Type u_1) [] [] :
theorem NumberField.discr_ne_zero (K : Type u_1) [] [] :
theorem NumberField.discr_eq_discr (K : Type u_1) [] [] {ι : Type u_2} [] [] (b : ) :
theorem NumberField.discr_eq_discr_of_algEquiv (K : Type u_1) [] [] {L : Type u_2} [] [] (f : K ≃ₐ[] L) :
theorem NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis (K : Type u_1) [] [] :
MeasureTheory.volume = * (NNReal.sqrt )
theorem NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr (K : Type u_1) [] [] (I : ) :
aI, a 0 | a| (FractionalIdeal.absNorm I) * * .factorial / * ||
theorem NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr (K : Type u_1) [] [] :
∃ (a : ), a 0 | a| * .factorial / * ||
theorem NumberField.abs_discr_ge {K : Type u_1} [] [] (h : ) :
4 / 9 * ( / 4) ^
theorem NumberField.abs_discr_gt_two {K : Type u_1} [] [] (h : ) :
2 <

Hermite-Minkowski Theorem. A nontrivial number field has discriminant greater than 2.

### Hermite Theorem #

This section is devoted to the proof of Hermite theorem.

Let N be an integer . We prove that the set S of finite extensions K of (in some fixed extension A of ) such that |discr K| ≤ N is finite by proving, using finite_of_finite_generating_set, that there exists a finite set T ⊆ A such that ∀ K ∈ S, ∃ x ∈ T, K = ℚ⟮x⟯ .

To find the set T, we construct a finite set T₀ of polynomials in ℤ[X] containing, for each K ∈ S, the minimal polynomial of a primitive element of K. The set T is then the union of roots in A of the polynomials in T₀. More precisely, the set T₀ is the set of all polynomials in ℤ[X] of degrees and coefficients bounded by some explicit constants depending only on N.

Indeed, we prove that, for any field K in S, its degree is bounded, see rank_le_rankOfDiscrBdd, and also its Minkowski bound, see minkowskiBound_lt_boundOfDiscBdd. Thus it follows from mixedEmbedding.exists_primitive_element_lt_of_isComplex and mixedEmbedding.exists_primitive_element_lt_of_isReal that there exists an algebraic integer x of K such that K = ℚ(x) and the conjugates of x are all bounded by some quantity depending only on N.

Since the primitive element x is constructed differently depending on wether K has a infinite real place or not, the theorem is proved in two parts.

theorem NumberField.hermiteTheorem.finite_of_finite_generating_set (A : Type u_2) [] [] {p : } (S : Set { F : // p F }) {T : Set A} (hT : T.Finite) (h : FS, xT, F = x) :
S.Finite
@[reducible, inline]

An upper bound on the degree of a number field K with |discr K| ≤ N, see rank_le_rankOfDiscrBdd.

Equations
Instances For
@[reducible, inline]

An upper bound on the Minkowski bound of a number field K with |discr K| ≤ N; see minkowskiBound_lt_boundOfDiscBdd.

Equations
• = NNReal.sqrt N * + 1
Instances For
theorem NumberField.hermiteTheorem.rank_le_rankOfDiscrBdd {K : Type u_1} [] [] {N : } (hK : N) :

If |discr K| ≤ N then the degree of K is at most rankOfDiscrBdd.

theorem NumberField.hermiteTheorem.minkowskiBound_lt_boundOfDiscBdd {K : Type u_1} [] [] {N : } (hK : N) :

If |discr K| ≤ N then the Minkowski bound of K is less than boundOfDiscrBdd.

theorem NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd {K : Type u_1} [] [] {N : } (hK : N) (a : ) (h : a = ) :
(minpoly a).natDegree
theorem NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal (A : Type u_2) [] [] (N : ) :
{K : { F : // } | {w : | w.IsReal}.Nonempty || N}.Finite
theorem NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex (A : Type u_2) [] [] (N : ) :
{K : { F : // } | {w : | w.IsComplex}.Nonempty || N}.Finite
theorem NumberField.finite_of_discr_bdd (A : Type u_2) [] [] (N : ) :
{K : { F : // } | || N}.Finite

Hermite Theorem. Let N be an integer. There are only finitely many number fields (in some fixed extension of ) of discriminant bounded by N.

@[simp]

The absolute discriminant of the number field is 1.

Alias of Rat.numberField_discr.

The absolute discriminant of the number field is 1.

theorem Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral {ι : Type u_2} {ι' : Type u_3} (K : Type u_1) [] [] [] [] [Fintype ι'] [] {b : Basis ι K} {b' : Basis ι' K} (h : ∀ (i : ι) (j : ι'), IsIntegral (b.toMatrix (b') i j)) (h' : ∀ (i : ι') (j : ι), IsIntegral (b'.toMatrix (b) i j)) :
=

If b and b' are -bases of a number field K such that ∀ i j, IsIntegral ℤ (b.toMatrix b' i j) and ∀ i j, IsIntegral ℤ (b'.toMatrix b i j) then discr ℚ b = discr ℚ b'.