Theorem conductor_mul_differentIdeal

Modification history

2025-06-09 15:24

Mathlib/RingTheory/DedekindDomain/Different.lean

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

Modified conductor_mul_differentIdeal View on Github →

2023-12-26 13:18

Mathlib/RingTheory/DedekindDomain/Different.lean

feat: derivative of minpoly is in the different ideal. (#9283)

Added conductor_mul_differentIdeal View on Github →