def Scheme.smoothLocus' (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] : Set ↥X

The smooth locus of a scheme: points where the local ring is regular.

theorem Scheme.mem_smoothLocus'_iff (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] (x : ↥X) : x ∈ smoothLocus' X ↔ IsRegularLocalRing ↑(X.presheaf.stalk x)

Membership in the smooth locus is equivalent to the stalk being a regular local ring.

theorem Scheme.smoothLocus'_isOpen (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] [AlgebraicGeometry.IsReduced X] [IrreducibleSpace ↥X] [Nonempty ↥X] : IsOpen (smoothLocus' X)

The smooth locus of a reduced irreducible scheme is open.

theorem Scheme.proposition30_smooth_locus_dense_open (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsLocallyNoetherian X] [AlgebraicGeometry.IsReduced X] [IrreducibleSpace ↥X] [Nonempty ↥X] : IsOpen (smoothLocus' X) ∧ Dense (smoothLocus' X) ∧ (smoothLocus' X).Nonempty

Proposition 30: the smooth locus of a reduced irreducible scheme is open, dense, and nonempty (containing the generic point).