Theorem PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation

Modification history

2025-04-02 12:19
Mathlib/RingTheory/Spectrum/Prime/Chevalley.lean
feat(RingTheory): Chevalley's theorem (#23571) …
Added PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentationView on Github →