Theorem Ideal.exists_ltSeries_length_eq_height

Modification history

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