Theorem PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim

Modification history

2025-04-06 21:39

Mathlib/RingTheory/Spectrum/Prime/Topology.lean

feat(PrimeSpectrum): Clopens in spectra of CommSemirings (#20533) …

Modified PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim View on Github →

2024-09-28 16:22

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

feat(RingTheory/Ideal/KrullDimension): define the Krull dimension of a ring (#14134) …

Added PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim View on Github →