Theorem PrimeSpectrum.preimage_specComap_zeroLocus

Modification history

2025-02-12 16:16

Mathlib/RingTheory/Spectrum/Prime/Basic.lean

chore(RingTheory/Spectrum/Prime/Basic): move functoriality to its own file (#21498)

Modified PrimeSpectrum.preimage_specComap_zeroLocus View on Github →

2024-09-24 20:52

Mathlib/RingTheory/PrimeSpectrum.lean

chore (PrimeSpectrum): `RingHom.primeComap` and API (#15114) …

Added PrimeSpectrum.preimage_specComap_zeroLocus View on Github →