Commit 2025-01-24 05:43 130893c2

View on Github →

feat: split a set in the prime spectrum of R[X] into its localization away from c : R and quotient by c parts (#20303) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Data/Set/Image.lean

added theorem Set.image_of_range_union_range_eq_univ

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

added theorem PrimeSpectrum.coe_comap

added theorem PrimeSpectrum.comap_apply

added theorem PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk