Theorem NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow

Modification history

2025-11-08 23:20
Mathlib/NumberTheory/NumberField/Discriminant/Different.lean
feat(NumberTheory): basic results about discriminants in an extension (#29940)
Added NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_powView on Github →