Commit 2025-09-02 13:33 f14dc2bc

feat(FractionalIdeal): define extended as a ring homomorphism (#28800) Define FractionalIdeal.extendedHom as the ring hom version of FractionalIdeal.extended and FractionalIdeal.extendedHomₐ to be the special version from fractional ideals of A to fractional ideals of B where A ⊆ B is an extension of commutative domains, so it's the special case where f := algebraMap A B. It is convenient to have both versions since, in the second version, the extra condition that the map must satisfied can be bundled.