Commit 2025-06-21 10:28 d1b53a66
View on Github →feat(RingTheory/KrullDimension/PID): remove domain condition in IsPrincipalIdealRing.krullDimLE_one (#25728)
feat(RingTheory/KrullDimension/PID): remove domain condition in IsPrincipalIdealRing.krullDimLE_one (#25728)