Theorem FractionalIdeal.coe_extendedHomₐ_eq_span

Modification history

2026-04-16 14:44
Mathlib/RingTheory/FractionalIdeal/Extended.lean
chore: rename FractionalIdeal.extendedHom (#38116) …
Deleted FractionalIdeal.coe_extendedHomₐ_eq_spanView on Github →
2025-10-24 05:21
Mathlib/RingTheory/FractionalIdeal/Extended.lean
feat(DedekindDomain): formulas for the different ideal in the compositum of disjoint extensions (#29770) …
Added FractionalIdeal.coe_extendedHomₐ_eq_spanView on Github →