Commit 2026-03-09 18:09 f07649fa

View on Github →

feat(Ringtheory/DedekindDomain): add RingEquiv lemmas (#35532) Co-authored by: @xgenereux.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Basic.lean

modified theorem Ring.DimensionLEOne.eq_bot_of_lt

modified theorem Ring.DimensionLEOne.isIntegralClosure

modified theorem Ring.DimensionLEOne.not_lt_lt

added theorem Ring.DimensionLEOne.of_ringEquiv

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

added theorem IsDedekindDomain.HeightOneSpectrum.RingEquiv.nontrivial_heightOneSpectrum

added def IsDedekindDomain.HeightOneSpectrum.comap

added def IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.eq_bot_of_comap_eq_bot'