Commit 2026-01-13 16:45 df6c5523

View on Github →

feat(RingTheory/Localization/Ideal): generalize comap_map_of_isPrime_disjoint to primary ideals (#33806) This PR generalizes comap_map_of_isPrime_disjoint to primary ideals, but keeps the existing statement around since it seems to be getting the most use in practice.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Height.lean

Modified Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/KrullDimension/Polynomial.lean

Modified Mathlib/RingTheory/Localization/AtPrime/Basic.lean

Modified Mathlib/RingTheory/Localization/Ideal.lean

added theorem IsLocalization.comap_map_of_isPrimary_disjoint

modified theorem IsLocalization.comap_map_of_isPrime_disjoint

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean