Commit 2025-06-09 15:24 d24f7121

View on Github →

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

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

modified theorem aeval_derivative_mem_differentIdeal

modified theorem coeIdeal_differentIdeal

modified theorem coeSubmodule_differentIdeal

modified theorem coeSubmodule_differentIdeal_fractionRing

modified theorem conductor_mul_differentIdeal

added theorem differentIdeal_ne_bot

modified theorem differentialIdeal_le_iff

added theorem not_dvd_differentIdeal_of_intTrace_not_mem

added theorem not_dvd_differentIdeal_of_isCoprime

added theorem not_dvd_differentIdeal_of_isCoprime_of_isSeparable

modified theorem pow_sub_one_dvd_differentIdeal

modified theorem pow_sub_one_dvd_differentIdeal_aux