Algebra.Smooth.isIntegrallyClosed_of_isDomain
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Smooth_isIntegrallyClosed_of_isDomain
universe uLean source · statement
theorem _root_.Algebra.Smooth.isIntegrallyClosed_of_isDomain (R : Type u) [CommRing R] [IsDomain R]
[IsIntegrallyClosed R]
(S : Type u) [CommRing S] [IsDomain S] [Algebra R S] [Algebra.Smooth R S] : IsIntegrallyClosed
S