Theorem NumberField.discr_dvd_discr

Modification history

2025-11-12 21:15
Mathlib/NumberTheory/NumberField/Discriminant/Different.lean
feat(NumberField): discriminant in disjoint extensions (#29943) …
Modified NumberField.discr_dvd_discrView on Github →
2025-11-08 23:20
Mathlib/NumberTheory/NumberField/Discriminant/Different.lean
feat(NumberTheory): basic results about discriminants in an extension (#29940)
Added NumberField.discr_dvd_discrView on Github →