Theorem FractionalIdeal.extendedHomₐ_injective

Modification history

2026-04-16 14:44

Mathlib/RingTheory/FractionalIdeal/Extended.lean

chore: rename FractionalIdeal.extendedHom (#38116) …

Deleted FractionalIdeal.extendedHomₐ_injective View on Github →

2025-11-16 17:26

Mathlib/RingTheory/FractionalIdeal/Extended.lean

feat(RingTheory/DedekindDomain): lifting an ideal in an extension is injective (#27244) …

Added FractionalIdeal.extendedHomₐ_injective View on Github →