2025-01-24 05:43
Mathlib/RingTheory/Spectrum/Prime/Topology.lean
feat: split a set in the prime spectrum of `R[X]` into its localization away from `c : R` and quotient by `c` parts (#20303) …
Added PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk