Theorem IsDedekindDomain.differentIdeal_eq_map_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.differentIdeal_eq_map_differentIdealView on Github →