Theorem Submodule.traceDual_le_span_map_traceDual

Modification history

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