Theorem not_dvd_differentIdeal_iff

Modification history

2025-06-19 11:54
Mathlib/RingTheory/DedekindDomain/Different.lean
feat(RingTheory/DedekindDomain): a prime divides the different ideal iff it is ramified (#25936)
Added not_dvd_differentIdeal_iffView on Github →