English
In a DVR, the maximal ideal is closed in the ambient topology; more precisely, the local maximal ideal yields a Hausdorff space when endowed with the valuation topology.
Русский
В DVR максимальный идеал замкнут в топологическом смысле; локальная структура порождает пространство Хаусдорфа в топологии оценки.
LaTeX
$$$\mathrm{IsHausdorff}(\mathrm{IsLocalRing.maximalIdeal}(R), R)$$$
Lean4
theorem addVal_le_iff_dvd {a b : R} : addVal R a ≤ addVal R b ↔ a ∣ b := by
classical
have hp := Classical.choose_spec (exists_prime R)
constructor <;> intro h
· by_cases ha0 : a = 0
· rw [ha0, addVal_zero, top_le_iff, addVal_eq_top_iff] at h
rw [h]
apply dvd_zero
obtain ⟨n, ha⟩ := associated_pow_irreducible ha0 hp.irreducible
rw [addVal, multiplicity_addValuation_apply, multiplicity_addValuation_apply,
emultiplicity_le_emultiplicity_iff] at h
exact ha.dvd.trans (h n ha.symm.dvd)
· rw [addVal, multiplicity_addValuation_apply, multiplicity_addValuation_apply]
exact emultiplicity_le_emultiplicity_of_dvd_right h
