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.

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

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

theorem NumberField.discr_eq_discr (K : Type u_1) [Field K] [NumberField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℤ (RingOfIntegers K)) : Algebra.discr ℤ ⇑b = 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) : discr K = discr L

@[simp]

theorem Rat.numberField_discr : NumberField.discr ℚ = 1

The absolute discriminant of the number field ℚ is 1.

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