Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace isRegularLocalRing_localization_atPrime_of_isStandardSmoothLean source · statement
theorem _root_.isRegularLocalRing_localization_atPrime_of_isStandardSmooth
(k B : Type*) [Field k] [CommRing B] [Algebra k B]
[Algebra.IsStandardSmooth k B] (q : Ideal B) [q.IsPrime] :
IsRegularLocalRing (Localization.AtPrime q)