Commit 2025-06-19 11:54 2239a8d3

View on Github →

feat(RingTheory/DedekindDomain): a prime divides the different ideal iff it is ramified (#25936)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

added theorem dvd_differentIdeal_iff

added theorem not_dvd_differentIdeal_iff

Modified Mathlib/RingTheory/Ideal/Over.lean

added theorem Ideal.Quotient.algebraMap_mk_of_liesOver

Modified Mathlib/RingTheory/LocalRing/ResidueField/Algebraic.lean

Created Mathlib/RingTheory/LocalRing/ResidueField/Instances.lean

added theorem Algebra.isSeparable_residueField_iff