Theorem Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown

Modification history

2025-11-30 11:46
Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean
feat(RingTheory/Height): height of ideal is height of preimage plus height in quotient (#27510) …
Added Ideal.height_eq_height_add_of_liesOver_of_hasGoingDownView on Github →