Theorem not_dvd_differentIdeal_of_isCoprime_of_isSeparable

Modification history

2025-06-09 15:24

Mathlib/RingTheory/DedekindDomain/Different.lean

feat(RingTheory/DedekindDomain): unramified primes does not divide differential (#25589)

Added not_dvd_differentIdeal_of_isCoprime_of_isSeparable View on Github →