Theorem PrimeSpectrum.coe_comap

Modification history

2025-12-15 09:35
Mathlib/RingTheory/Spectrum/Prime/Topology.lean
chore(RingTheory): rename `RingHom.specComap` to `PrimeSpectrum.comap` (#32703) …
Deleted PrimeSpectrum.coe_comapView on Github →
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.coe_comapView on Github →