Theorem IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_exists

Modification history

2025-07-07 22:34
Mathlib/RingTheory/DedekindDomain/Ideal.lean
chore: tidy various files (#26883)
Modified IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_existsView on Github →
2025-06-12 12:52
Mathlib/RingTheory/DedekindDomain/Ideal.lean
feat(RingTheory/Ideal/Maximal): `ne_top_iff_exists_maximal` (#25331) …
Added IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_existsView on Github →