Theorem IsLocalization.comap_map_of_isPrimary_disjoint

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_map_of_isPrimary_disjoint View on Github →

2026-01-13 16:45

Mathlib/RingTheory/Localization/Ideal.lean

feat(RingTheory/Localization/Ideal): generalize `comap_map_of_isPrime_disjoint` to primary ideals (#33806) …

Added IsLocalization.comap_map_of_isPrimary_disjoint View on Github →