Commit 2025-09-12 23:46 93fccc93
View on Github →feat(RingTheory/Ideal/Height): sup of ideal heights equals Krull dimension (#27825)
Adds Ideal.sup_height_eq_ringKrullDim and Ideal.sup_primeHeight_eq_ringKrullDim.
They show the suprema of heights of ideals / prime ideals are equal to the Krull dimension, when the ring is nonzero.