Theorem NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow

Modification history

2025-11-12 21:15
Mathlib/NumberTheory/NumberField/Discriminant/Different.lean
feat(NumberField): discriminant in disjoint extensions (#29943) …
Added NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_powView on Github →