isIntegrallyClosed — Mathlib

English

If A is a Dedekind DVR, then A is integrally closed.

Русский

Если A — Dedekind DVR, то A интегрально замкнуто.

LaTeX

$$$\text{IsIntegrallyClosed } A$$$

Lean4

instance isIntegrallyClosed [h : IsDedekindDomainDvr A] : IsIntegrallyClosed A :=
  IsIntegrallyClosed.of_localization_maximal <| fun p hp0 hpm ↦
    let ⟨_, _⟩ :=
      (IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime (Localization.AtPrime p)).mp
        (h.is_dvr_at_nonzero_prime p hp0 hpm.isPrime)
    inferInstance

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