Documentation

Mathlib.NumberTheory.NumberField.Discriminant

Number field discriminant #

This file defines the discriminant of a number field.

Main definitions #

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.

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 ι ℤ { x // x ∈ NumberField.ringOfIntegers K }) :
    Algebra.discr ℤ ↑b = NumberField.discr K
    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.