Commit 2023-09-01 13:27 b5fcdfd9

View on Github →

feat: define the discriminant of a number field (#6394) This PR defines the discriminant of a number field as the discriminant of RingOfIntegers.basis and proves some basic results, mainly: it does not depend upon the choice of the integral basis and it is equal to 1 for ℚ.

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/NumberField/Discriminant.lean

added theorem NumberField.coe_discr

added theorem NumberField.discr_eq_discr

added theorem NumberField.discr_ne_zero

added theorem Rat.numberField_discr