Commit 2025-11-08 23:20 88f8b727

View on Github →

feat(NumberTheory): basic results about discriminants in an extension (#29940)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Discriminant/Different.lean

modified theorem NumberField.absNorm_differentIdeal

added theorem NumberField.discr_dvd_discr

modified theorem NumberField.discr_mem_differentIdeal

added theorem NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow