Regular local rings are domains

TheoremExistence of a parameter avoiding minimal primes and the square#✓fully proved

In a Noetherian local ring of positive Krull dimension, there is a parameter in the maximal ideal, outside its square and outside every minimal prime.

theorem IsLocalRing.exists_mem_maximalIdeal_notMem_sq_forall_minimalPrimes_notMem
    (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    (hdim : 0 < ringKrullDim R) :
    ∃ x ∈ maximalIdeal R, x ∉ (maximalIdeal R) ^ 2 ∧
      ∀ p ∈ minimalPrimes R, x ∉ p

Used by 2

Used byRegular local rings are domains · Regular local rings of dimension at most two are UFDs

TheoremRegular local rings are domains#✓fully proved

Every regular local ring is a domain.

theorem IsRegularLocalRing.isDomain (R : Type*) [CommRing R] [IsRegularLocalRing R] :
    IsDomain R

Uses 2 · Used by 1

Proof usesExistence of a parameter avoiding minimal primes and the square · Quotient of a regular local ring by a regular parameter is regular

Used byRegular local rings of dimension at most two are UFDs

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.