Def IsDedekindDomain.HeightOneSpectrum.comap

Modification history

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