instIsHausdorffMaximalIdeal — Mathlib

English

Hausdorff property of maximal ideal is established via valuation inequalities in DVRs.

Русский

Свойство Хаусдорфа максимального идеала устанавливается через неравенства оценки в DVR.

LaTeX

$$$\mathrm{IsHausdorff}(\mathrm{IsLocalRing.maximalIdeal}(R), R)$$$

Lean4

instance (R : Type*) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R] : IsHausdorff (maximalIdeal R) R where
  haus' x
    hx := by
    obtain ⟨ϖ, hϖ⟩ := exists_irreducible R
    simp only [← Ideal.one_eq_top, smul_eq_mul, mul_one, SModEq.zero, hϖ.maximalIdeal_eq, Ideal.span_singleton_pow,
      Ideal.mem_span_singleton, ← addVal_le_iff_dvd, hϖ.addVal_pow] at hx
    rwa [← addVal_eq_top_iff, WithTop.eq_top_iff_forall_ge]

Похожие утверждения