Theorem Ideal.ne_top_iff_exists_maximal

Modification history

2025-06-12 12:52
Mathlib/RingTheory/Ideal/Maximal.lean
feat(RingTheory/Ideal/Maximal): `ne_top_iff_exists_maximal` (#25331) …
Added Ideal.ne_top_iff_exists_maximalView on Github →