Theorem IsDedekindDomain.HeightOneSpectrum.RingEquiv.nontrivial_heightOneSpectrum

Modification history

2026-03-09 18:09
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
feat(Ringtheory/DedekindDomain): add RingEquiv lemmas (#35532) …
Added IsDedekindDomain.HeightOneSpectrum.RingEquiv.nontrivial_heightOneSpectrumView on Github →