Theorem NumberField.discr_mem_differentIdeal

Modification history

2025-11-08 23:20
Mathlib/NumberTheory/NumberField/Discriminant/Different.lean
feat(NumberTheory): basic results about discriminants in an extension (#29940)
Modified NumberField.discr_mem_differentIdealView on Github →
2025-06-14 13:55
Mathlib/NumberTheory/NumberField/Discriminant/Different.lean
feat(NumberTheory): discriminant is norm of different (#25792)
Added NumberField.discr_mem_differentIdealView on Github →