AlgebraicGeometry.Smooth.isRegularLocalRing_stalk
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_isRegularLocalRing_stalk
universe u
open CategoryTheory AlgebraicGeometry IsLocalRingLean source · statement
theorem _root_.AlgebraicGeometry.Smooth.isRegularLocalRing_stalk
{k : Type u} [Field k] {X : Scheme.{u}} {f : X ⟶ Spec (CommRingCat.of k)}
[Smooth f] (x : X) :
IsRegularLocalRing (X.presheaf.stalk x)