Theorem FractionalIdeal.dual_eq_dual_mul_dual

Modification history

2025-10-19 08:57

Mathlib/RingTheory/DedekindDomain/Different.lean

feat(DedekindDomain/Different): add the transitivity formula (#26155) …

Added FractionalIdeal.dual_eq_dual_mul_dual View on Github →