Number field discriminant

This file defines the discriminant of a number field.

Main definitions

• NumberField.discr: the absolute discriminant of a number field.

Tags

number field, discriminant

@[reducible, inline]

noncomputable abbrev NumberField.discr (K : Type u_1) [Field K] [NumberField K] : ℤ

The absolute discriminant of a number field.

Equations

• NumberField.discr K = Algebra.discr ℤ ⇑(NumberField.RingOfIntegers.basis K)

theorem NumberField.coe_discr (K : Type u_1) [Field K] [NumberField K] : ↑(NumberField.discr K) = Algebra.discr ℚ ⇑(NumberField.integralBasis K)

theorem NumberField.discr_ne_zero (K : Type u_1) [Field K] [NumberField K] : NumberField.discr K ≠ 0

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

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

@[simp]

theorem Rat.numberField_discr : NumberField.discr ℚ = 1

The absolute discriminant of the number field ℚ is 1.

theorem NumberField.discr_rat : NumberField.discr ℚ = 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) [Field K] [DecidableEq ι] [DecidableEq ι'] [Fintype ι] [Fintype ι'] [NumberField K] {b : Basis ι ℚ K} {b' : Basis ι' ℚ K} (h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)) (h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (b'.toMatrix (⇑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'.