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