Theorem FractionalIdeal.le_one_of_extendedHomₐ_le_one

Modification history

2026-04-16 14:44

Mathlib/RingTheory/FractionalIdeal/Extended.lean

chore: rename FractionalIdeal.extendedHom (#38116) …

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