Theorem FractionalIdeal.extended_le_one_of_le_one

Modification history

2025-10-24 05:21
Mathlib/RingTheory/FractionalIdeal/Extended.lean
feat(DedekindDomain): formulas for the different ideal in the compositum of disjoint extensions (#29770) …
Added FractionalIdeal.extended_le_one_of_le_oneView on Github →