Theorem FractionalIdeal.one_le_extendedHomₐ_iff

Modification history

2026-04-16 14:44

Mathlib/RingTheory/FractionalIdeal/Extended.lean

chore: rename FractionalIdeal.extendedHom (#38116) …

Deleted FractionalIdeal.one_le_extendedHomₐ_iff 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.one_le_extendedHomₐ_iff View on Github →