Algebra.Smooth.of_isIntegrallyClosed_of_krullDimLE_one_of_perfectField
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Smooth_of_isIntegrallyClosed_of_krullDimLE_one_of_perfectField
universe u v
open IsLocalRingLean source · statement
theorem _root_.Algebra.Smooth.of_isIntegrallyClosed_of_krullDimLE_one_of_perfectField
(k : Type u) [Field k] [PerfectField k] (B : Type v) [CommRing B] [IsDomain B] [Algebra k B]
[Algebra.FiniteType k B] [IsIntegrallyClosed B] [Ring.KrullDimLE 1 B] :
Algebra.Smooth k B