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) …
Added IsDedekindDomain.range_sup_range_eq_top_of_isCoprime_differentIdeal