mathlib

42dda89e - feat(ring_theory/discrete_valuation_ring): is_Hausdorff (#8994)

feat(ring_theory/discrete_valuation_ring): is_Hausdorff (#8994) Discrete valuation rings are Hausdorff in the algebraic sense that the intersection of all powers of the maximal ideal is 0.