NYLL
Module

Algebra_Smooth_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_Smooth_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
1 declaration indexed from sourceView source ↗

Module documentation

Algebra Smooth is Domain and is Integrally Closed of is Localization at Prime

Imports4
Imported by2

Declarations

theorem

isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime

L29 ↗
Algebra.Smooth.isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Smooth_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
universe u
Lean source · statement
theorem _root_.Algebra.Smooth.isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
    (R : Type u) [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R]
    (S : Type u) [CommRing S] [Algebra R S] [Algebra.Smooth R S]
    (p : Ideal S) [p.IsPrime] (Sₚ : Type u) [CommRing Sₚ] [Algebra S Sₚ] [IsLocalization.AtPrime Sₚ
      p] :
    IsDomain Sₚ ∧ IsIntegrallyClosed Sₚ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.