AlgebraicCurves.Geometry.Curves.Proofs.geometricallyIntegral_of_smooth_of_geometricallyConnected.GeomIntKit.isIntegral_of_smooth_of_connectedSpace
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace geometricallyIntegral_of_smooth_of_geometricallyConnected
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace GeomIntKitLean source · statement
theorem isIntegral_of_smooth_of_connectedSpace {K : Type u} [Field K] {X : Scheme.{u}}
(t : X ⟶ Spec (CommRingCat.of K)) [Smooth t] [ConnectedSpace X] : IsIntegral X