Commit 2026-04-16 14:44 23c1716f

View on Github →

chore: rename FractionalIdeal.extendedHom (#38116) We rename FractionalIdeal.extendedHomₐ to FractionalIdeal.extendedHom, since this looks the most natural application, and FractionalIdeal.extendedHom to FractionalIdeal.extendedHom'.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/LinearDisjoint.lean

Modified Mathlib/RingTheory/FractionalIdeal/Extended.lean

added theorem FractionalIdeal.coe_extendedHom_eq_span

deleted theorem FractionalIdeal.coe_extendedHomₐ_eq_span

added def FractionalIdeal.extendedHom'

deleted def FractionalIdeal.extendedHom

added theorem FractionalIdeal.extendedHom_coeIdeal_eq_map

added theorem FractionalIdeal.extendedHom_eq_one_iff

added theorem FractionalIdeal.extendedHom_eq_zero_iff

added theorem FractionalIdeal.extendedHom_injective

added theorem FractionalIdeal.extendedHom_le_one_iff

deleted theorem FractionalIdeal.extendedHomₐ_coeIdeal_eq_map

deleted theorem FractionalIdeal.extendedHomₐ_eq_one_iff

deleted theorem FractionalIdeal.extendedHomₐ_eq_zero_iff

deleted theorem FractionalIdeal.extendedHomₐ_injective

deleted theorem FractionalIdeal.extendedHomₐ_le_one_iff

added theorem FractionalIdeal.le_one_of_extendedHom_le_one

deleted theorem FractionalIdeal.le_one_of_extendedHomₐ_le_one

added theorem FractionalIdeal.one_le_extendedHom_iff

deleted theorem FractionalIdeal.one_le_extendedHomₐ_iff