Commit 2025-03-13 07:17 b6284ef3

feat(RingTheory/Ideal): more lemmas about the height of an ideal (#21041) In this PR, we continue to port a part of Andrew Yang's lean3 repository at this repository, which is appoved by @erdOne after his discussion with @chrisflav . This PR follows #20741 (merged by Bors) and #20744. We ported Andrew's definition of Ideal.height and Ideal.primeHeight with some small changes in #20741, and in this PR, we ported some more lemmas about these definitions, finishing the porting work of dimension_theory/height.lean in that repository.

• depends on: #20744 [some of the lemmas used spanRank]
• depends on: #22236 [We separated the lemmas about Order.height and krullDim to this PR] @erdOne @Xuchun-Li li.xuchun@qq.com @jjdishere emailboxofjjd@163.com @Blackfeather007 2100017455@stu.pku.edu.cn @ShouxinZhang 202013140018@nuist.edu.cn