Documentation

Mathlib.NumberTheory.NumberField.Discriminant

Number field discriminant #

This file defines the discriminant of a number field.

Main definitions #

Main result #

Tags #

number field, discriminant

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

The absolute discriminant of a number field.

Equations
Instances For
    source
    theorem NumberField.coe_discr (K : Type u_1) [Field K] [NumberField K] :
    ↑(NumberField.discr K) = Algebra.discr ℚ ⇑(NumberField.integralBasis K)
    source
    theorem NumberField.discr_ne_zero (K : Type u_1) [Field K] [NumberField K] :
    NumberField.discr K ≠ 0
    source
    theorem NumberField.discr_eq_discr (K : Type u_1) [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι ℤ ↥(NumberField.ringOfIntegers K)) :
    Algebra.discr ℤ ⇑b = NumberField.discr K
    source
    theorem NumberField.discr_eq_discr_of_algEquiv (K : Type u_1) [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] (f : K ≃ₐ[ℚ] L) :
    NumberField.discr K = NumberField.discr L
    source
    theorem NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis (K : Type u_1) [Field K] [NumberField K] :
    ↑↑MeasureTheory.volume (Zspan.fundamentalDomain (NumberField.mixedEmbedding.latticeBasis K)) = 2⁻¹ ^ NumberField.InfinitePlace.NrComplexPlaces K * ↑(NNReal.sqrt ‖NumberField.discr K‖₊)
    source
    theorem NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors ↥(NumberField.ringOfIntegers K)) K)ˣ) :
    ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ ↑(FractionalIdeal.absNorm ↑I) * (4 / Real.pi) ^ NumberField.InfinitePlace.NrComplexPlaces K * ↑(Nat.factorial (FiniteDimensional.finrank ℚ K)) / ↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K * Real.sqrt |↑(NumberField.discr K)|
    source
    theorem NumberField.exists_ne_zero_mem_ringOfIntegers_of_norm_le_mul_sqrt_discr (K : Type u_1) [Field K] [NumberField K] :
    ∃ (a : ↥(NumberField.ringOfIntegers K)), a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (4 / Real.pi) ^ NumberField.InfinitePlace.NrComplexPlaces K * ↑(Nat.factorial (FiniteDimensional.finrank ℚ K)) / ↑(FiniteDimensional.finrank ℚ K) ^ FiniteDimensional.finrank ℚ K * Real.sqrt |↑(NumberField.discr K)|
    source
    theorem NumberField.abs_discr_ge {K : Type u_1} [Field K] [NumberField K] (h : 1 < FiniteDimensional.finrank ℚ K) :
    4 / 9 * (3 * Real.pi / 4) ^ FiniteDimensional.finrank ℚ K ≤ ↑|NumberField.discr K|
    source
    theorem NumberField.abs_discr_gt_two {K : Type u_1} [Field K] [NumberField K] (h : 1 < FiniteDimensional.finrank ℚ K) :
    2 < |NumberField.discr K|

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

    source
    @[simp]
    theorem Rat.numberField_discr :
    NumberField.discr ℚ = 1

    The absolute discriminant of the number field ℚ is 1.

    source
    theorem NumberField.discr_rat :
    NumberField.discr ℚ = 1

    Alias of Rat.numberField_discr.

    The absolute discriminant of the number field ℚ is 1.

    source
    theorem Algebra.discr_eq_discr_of_toMatrix_coeff_isIntegral {ι : Type u_2} {ι' : Type u_3} (K : Type u_1) [Field K] [DecidableEq ι] [DecidableEq ι'] [Fintype ι] [Fintype ι'] [NumberField K] {b : Basis ι ℚ K} {b' : Basis ι' ℚ K} (h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (Basis.toMatrix b (⇑b') i j)) (h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (Basis.toMatrix b' (⇑b) i j)) :
    Algebra.discr ℚ ⇑b = Algebra.discr ℚ ⇑b'

    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'.