Commit 2025-06-12 12:52 54c2be31

View on Github →

feat(RingTheory/Ideal/Maximal): ne_top_iff_exists_maximal (#25331) We add Ideal.ne_top_iff_exists_maximal and an analogous statement for IsDedekindDomain.HeightOneSpectrum.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

added theorem IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_exists

Modified Mathlib/RingTheory/Ideal/Maximal.lean

added theorem Ideal.ne_top_iff_exists_maximal