Def FractionalIdeal.extendedHom

Modification history

2026-04-16 14:44
Mathlib/RingTheory/FractionalIdeal/Extended.lean
chore: rename FractionalIdeal.extendedHom (#38116) …
Deleted FractionalIdeal.extendedHomView on Github →
2025-09-02 13:33
Mathlib/RingTheory/FractionalIdeal/Extended.lean
feat(FractionalIdeal): define `extended` as a ring homomorphism (#28800) …
Added FractionalIdeal.extendedHomView on Github →