Commit 2025-05-11 19:52 27a83846
View on Github →feat(RingTheory/Ideal/Height): Krull height theorem (#23778) In this PR, we continue to port @erdOne 's lean3 repository at here, and (finally!) finished the result of Krull's height theorem. This PR is a refactor of #22403 where the code diverged from upstream due to newly merged PRs. Andrew Yang @erdOne Wanyi He @Blackfeather007 2100017455@stu.pku.edu.cn Shouxin Zhang @ShouxinZhang 202013140018@nuist.edu.cn Jiedong Jiang @jjdishere emailboxofjjd@163.com