Theorem Module.Basis.ofIsCoprimeDifferentIdeal_apply

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 Module.Basis.ofIsCoprimeDifferentIdeal_applyView on Github →