Mathlib Changelog
v4
Changelog
About
Github
Theorem
Ideal.height_le_ringKrullDim_quotient_add_one
Modification history
2026-01-22 07:06
Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean
feat(RingTheory/KrullDimension): generalize some results about local rings (#27557) …
Added
Ideal.height_le_ringKrullDim_quotient_add_one
View on Github →