Commit 2025-11-30 11:46 54343569
View on Github →feat(RingTheory/Height): height of ideal is height of preimage plus height in quotient (#27510)
If S has going-down over R, the height of a prime P lying over p equals the height of p plus the height of the image of P in S / p S.
Co-authored by: Sihan Su ssh@stu.pku.edu.cn
Co-authored by: Yi Song sif4delta0@mail.ustc.edu.cn