Commit 2023-11-30 20:26 c799ea08

View on Github →

feat: two isomorphic number fields have the same discriminant (#8714)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Discriminant.lean

added theorem NumberField.discr_eq_discr_of_algEquiv

Modified Mathlib/RingTheory/Discriminant.lean

added theorem Algebra.discr_eq_discr_of_algEquiv

Modified Mathlib/RingTheory/IntegralClosure.lean

added def integralClosure_algHom_restrict

added theorem integralClosure_coe_algEquiv_restrict

added theorem integralClosure_coe_algHom_restrict