Commit 2025-11-16 17:26 2628d8c4
View on Github →feat(RingTheory/DedekindDomain): lifting an ideal in an extension is injective (#27244)
This PR develops some API for FractionalIdeal.extendedHomₐ and in particular proves when it is an injective map. As a consequence, it deduces the fact that lifting an integral ideal in an extension of Dedekind domains is an injective map.
Note: the import increase happens in a leaf file Mathlib.RingTheory.FractionalIdeal.Extended