Commit 2025-01-20 10:56 1b34e3c4
View on Github →feat(RingTheory/Ideal): the height of an ideal (#20741)
In this PR, we ported a part of Andrew Yang's lean3 repository at this repository, which is appoved by @erdOne after his discussion with @chrisflav .
Andrew defined Ideal.primeHeight and Ideal.height in this repository (it's at /dimension_theory/height), we ported this, changed the definition of Ideal.primeHeight to Order.height (⟨I, hI⟩ : PrimeSpectrum R) and ported some basic lemmas about it.
@erdOne
@Xuchun-Li li.xuchun@qq.com
@jjdishere emailboxofjjd@163.com
@Blackfeather007 2100017455@stu.pku.edu.cn