Theorem FractionalIdeal.extendedHomₐ_coeIdeal_eq_map

Modification history

2026-04-16 14:44
Mathlib/RingTheory/FractionalIdeal/Extended.lean
chore: rename FractionalIdeal.extendedHom (#38116) …
Deleted FractionalIdeal.extendedHomₐ_coeIdeal_eq_mapView on Github →
2025-10-19 08:57
Mathlib/RingTheory/FractionalIdeal/Extended.lean
feat(DedekindDomain/Different): add the transitivity formula (#26155) …
Added FractionalIdeal.extendedHomₐ_coeIdeal_eq_mapView on Github →