Theorem FractionalIdeal.differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprime

Modification history

2025-11-05 09:57
Mathlib/RingTheory/DedekindDomain/LinearDisjoint.lean
feat(DedekindDomain): lift a basis in a disjoint extension when the different ideals are coprime (#29885) …
Deleted FractionalIdeal.differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprimeView on Github →
2025-10-24 05:21
Mathlib/RingTheory/DedekindDomain/LinearDisjoint.lean
feat(DedekindDomain): formulas for the different ideal in the compositum of disjoint extensions (#29770) …
Added FractionalIdeal.differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprimeView on Github →