Theorem coeIdeal_differentIdeal

Modification history

2025-06-09 15:24

Mathlib/RingTheory/DedekindDomain/Different.lean

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

Modified coeIdeal_differentIdeal View on Github →

2023-12-19 15:21

Mathlib/RingTheory/DedekindDomain/Different.lean

feat: Define the different ideal. (#9063)

Added coeIdeal_differentIdeal View on Github →