Commit 2023-12-19 15:21 45a5e1b4

View on Github →

feat: Define the different ideal. (#9063)

Estimated changes

Modified Mathlib/FieldTheory/Separable.lean

added theorem IsSeparable.of_equiv_equiv

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

added theorem coeIdeal_differentIdeal

added theorem coeSubmodule_differentIdeal

added theorem coeSubmodule_differentIdeal_fractionRing

added def differentIdeal

added theorem differentialIdeal_le_fractionalIdeal_iff

added theorem differentialIdeal_le_iff

added theorem map_equiv_traceDual

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

added theorem FractionalIdeal.inv_le_comm

added theorem FractionalIdeal.le_inv_comm

Modified Mathlib/RingTheory/Finiteness.lean

added theorem Module.Finite.of_equiv_equiv

Modified Mathlib/RingTheory/IntegrallyClosed.lean

added theorem IsIntegralClosure.of_isIntegrallyClosed