Algebra.IsSmoothAt.flat_localization_atPrime
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_IsSmoothAt_flat_localization_atPrime
open AlgebraLean source · statement
theorem _root_.Algebra.IsSmoothAt.flat_localization_atPrime (R A : Type) [CommRing R] [CommRing A]
[Algebra R A]
[Algebra.FinitePresentation R A] (p : Ideal A) [p.IsPrime] [Algebra.IsSmoothAt R p] :
Module.Flat R (Localization.AtPrime p)