Theorem pow_sub_one_dvd_differentIdeal_aux

Modification history

2025-06-09 15:24
Mathlib/RingTheory/DedekindDomain/Different.lean
feat(RingTheory/DedekindDomain): unramified primes does not divide differential (#25589)
Modified pow_sub_one_dvd_differentIdeal_auxView on Github →
2024-10-25 15:28
Mathlib/RingTheory/DedekindDomain/Different.lean
feat: add pow_sub_one_dvd_differentIdeal (#18228) …
Added pow_sub_one_dvd_differentIdeal_auxView on Github →