Commit 2025-02-05 10:58 76560a8a

View on Github →

feat(RingTheory): Ring.KrullDimLE type class (#21452) Also split RingTheory/Ideal/MinimalPrimes.lean into RingTheory/Ideal/MinimalPrimes/Basic.lean and RingTheory/Ideal/MinimalPrimes/Localization.lean.

Estimated changes

added theorem Order.KrullDimLE.mono
added def minimalPrimes
deleted theorem Ideal.minimalPrimes_top
deleted theorem Ideal.sInf_minimalPrimes
deleted def minimalPrimes
deleted theorem minimalPrimes_eq_minimals
added theorem Ring.KrullDimLE.mk₀
added theorem Ring.KrullDimLE.mk₁'
added theorem Ring.KrullDimLE.mk₁
modified theorem ringKrullDim_quotient_le
deleted theorem PrimeSpectrum.isMax_iff
deleted theorem PrimeSpectrum.isMin_iff