Theorem not_dvd_differentIdeal_of_intTrace_not_mem

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_intTrace_not_mem View on Github →