Def IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv

Modification history

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