Theorem IsLocalization.comap_le_comap_iff

Modification history

2026-05-12 12:43

Mathlib/RingTheory/Localization/Ideal.lean

chore(RingTheory/Localization/AtPrime/Basic): use `under` instead of `comap (algebraMap R S)` (#37840) …

Deleted IsLocalization.comap_le_comap_iff View on Github →

2026-03-26 08:33

Mathlib/RingTheory/Localization/Ideal.lean

feat(RingTheory/Unramified/Dedekind): a domain finite and unramified over a Dedekind domain is a Dedekind domain (#36838) …

Added IsLocalization.comap_le_comap_iff View on Github →