Module

IsRegularLocalRing_isDomain_and_isIntegrallyClosed_of_ringKrullDim_le_one.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.IsRegularLocalRing_isDomain_and_isIntegrallyClosed_of_ringKrullDim_le_one

1 declaration indexed from sourceView source ↗

Module documentation

Is Regular Local Ring is Domain and is Integrally Closed of ring Krull Dim le one

Imports1

Mathlib.RingTheory.RegularLocalRing.Defs

Imported by2

theorem

isDomain_and_isIntegrallyClosed_of_ringKrullDim_le_one

L25 ↗

IsRegularLocalRing.isDomain_and_isIntegrallyClosed_of_ringKrullDim_le_one

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace IsRegularLocalRing_isDomain_and_isIntegrallyClosed_of_ringKrullDim_le_one
open IsLocalRing in

Lean source · statement

theorem _root_.IsRegularLocalRing.isDomain_and_isIntegrallyClosed_of_ringKrullDim_le_one
    (A : Type*) [CommRing A] [IsRegularLocalRing A] (h : ringKrullDim A ≤ 1) :
    IsDomain A ∧ IsIntegrallyClosed A

Module documentation

Is Regular Local Ring is Domain and is Integrally Closed of ring Krull Dim le one

Declarations

isDomain_and_isIntegrallyClosed_of_ringKrullDim_le_one