Commit 2023-06-03 07:38 4d80fbff

View on Github →

feat: port RingTheory.DedekindDomain.Basic (#4608)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/DedekindDomain/Basic.lean

added theorem Ring.DimensionLEOne.eq_bot_of_lt

added theorem Ring.DimensionLEOne.isIntegralClosure

added theorem Ring.DimensionLEOne.not_lt_lt

added theorem Ring.DimensionLEOne.principal_ideal_ring

added def Ring.DimensionLEOne

added theorem isDedekindDomain_iff

Modified Mathlib/RingTheory/Polynomial/RationalRoot.lean