Commit 2023-12-26 13:40 2d7e88a5

View on Github →

feat: A dedekind domain that is local is a PID. (#9282)

Estimated changes

Modified Mathlib/RingTheory/Artinian.lean

Modified Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

added theorem LocalRing.finrank_CotangentSpace_eq_one

added theorem LocalRing.finrank_CotangentSpace_eq_one_iff

added theorem tfae_of_isNoetherianRing_of_localRing_of_isDomain

Modified Mathlib/RingTheory/Filtration.lean

added theorem Ideal.isIdempotentElem_iff_eq_bot_or_top_of_localRing

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

added theorem LocalRing.CotangentSpace.map_eq_top_iff

added theorem LocalRing.CotangentSpace.span_image_eq_top_iff

added theorem LocalRing.finrank_cotangentSpace_eq_zero

added theorem LocalRing.finrank_cotangentSpace_eq_zero_iff

added theorem LocalRing.finrank_cotangentSpace_le_one_iff

added theorem LocalRing.subsingleton_cotangentSpace_iff

Modified Mathlib/RingTheory/Nakayama.lean

Modified Mathlib/RingTheory/Valuation/ValuationRing.lean

modified theorem ValuationRing.iff_local_bezout_domain