Def differentIdeal

Modification history

2025-05-02 23:00

Mathlib/RingTheory/DedekindDomain/Different.lean

chore: bump toolchain to v4.20.0-rc2 (#24561)

Deleted differentIdeal View on Github →

2023-12-19 15:21

Mathlib/RingTheory/DedekindDomain/Different.lean

feat: Define the different ideal. (#9063)

Added differentIdeal View on Github →