Commit 2024-08-21 11:51 559b6a5e

feat(Mathlib.RingTheory.FractionalIdeal.Extended): Define extensions of fractional ideals (#14216) Define the extension of a fractional ideal along a ring homomorphism, and prove some basic facts about extensions. This PR is part 2/4 of a proof of isDedekindDomain_iff_isDedekindDomainDvr. Part 1: #14099 Part 3: #14237 Part 4: #14242

• depends on: #14099