Commit 2026-05-22 17:40 33390a7d

refactor(RingTheory/Ideal/Height): make Ideal.primeHeight private (#37627) We mark Ideal.primeHeight as private, making Ideal.height the only public definition for heights of (prime) ideals. This makes the API more consistent and stops contributors from adding more declarations involving Ideal.primeHeight, which should instead be formulated in terms of Ideal.height. To relate Ideal.height to the order theoretic Order.height in the lattice of prime ideals PrimeSpectrum we add a lemma PrimeSpectrum.height_eq_orderHeight.