Theorem differentIdeal_eq_differentIdeal_mul_differentIdeal

Modification history

2025-10-19 08:57
Mathlib/RingTheory/DedekindDomain/Different.lean
feat(DedekindDomain/Different): add the transitivity formula (#26155) …
Added differentIdeal_eq_differentIdeal_mul_differentIdealView on Github →