Commit 2023-06-08 04:34 cabed4d3

View on Github →

feat: port RingTheory.DiscreteValuationRing.TFAE (#4825)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/DedekindDomain/Basic.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

added theorem IsDedekindDomainInv.dimensionLEOne

deleted theorem IsDedekindDomainInv.dimensionLeOne

Created Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

added theorem DiscreteValuationRing.TFAE

added theorem exists_maximalIdeal_pow_eq_of_principal

added theorem maximalIdeal_isPrincipal_of_isDedekindDomain