Theorem FractionalIdeal.trace_mem_dual_one

Modification history

2025-10-19 08:57

Mathlib/RingTheory/DedekindDomain/Different.lean

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

Added FractionalIdeal.trace_mem_dual_one View on Github →