Theorem Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint

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 Submodule.traceDual_eq_span_map_traceDual_of_linearDisjointView on Github →