Theorem IsDedekindDomain.map_differentIdeal_dvd_differentIdeal

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) …
Added IsDedekindDomain.map_differentIdeal_dvd_differentIdealView on Github →