Theorem ValuationRing.iff_local_bezout_domain

Modification history

2023-12-26 13:40
Mathlib/RingTheory/Valuation/ValuationRing.lean
feat: A dedekind domain that is local is a PID. (#9282)
Modified ValuationRing.iff_local_bezout_domainView on Github →
2023-06-06 12:22
Mathlib/RingTheory/Valuation/ValuationRing.lean
feat: port RingTheory.Valuation.ValuationRing (#4720)
Added ValuationRing.iff_local_bezout_domainView on Github →