Smooth

📁 Source: Mathlib/AlgebraicGeometry/Group/Smooth.lean

Statistics

Metric	Count
Definitions	0
Theorems smooth_of_grpObj_of_isAlgClosed	1
Total	1

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smooth_of_grpObj_of_isAlgClosed 📖	mathematical	—	Smooth Spec CommRingCat.of EuclideanDomain.toCommRing Field.toEuclideanDomain	—	LocallyOfFiniteType.jacobsonSpace instLocallyOfFiniteTypeOfLocallyOfFinitePresentation instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing instIsJacobsonRingOfKrullDimLEOfNatNat PrimeSpectrum.instKrullDimLEOfNatNat isArtinian_of_fg_of_artinian' DivisionRing.instIsArtinianRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self Field.instIsLocalRing Scheme.Hom.smoothLocus_eq_top_iff TopologicalSpace.Opens.coe_eq_univ not_ne_iff Set.nonempty_compl nonempty_inter_closedPoints IsClosed.isLocallyClosed IsOpen.isClosed_compl TopologicalSpace.Opens.is_open' Dense.nonempty Scheme.Hom.dense_smoothLocus_of_perfectField IsAlgClosed.perfectField IsOpen.isLocallyClosed CategoryTheory.Category.assoc CategoryTheory.Iso.eq_comp_inv CategoryTheory.CartesianMonoidalCategory.comp_lift_assoc CategoryTheory.Category.comp_id CategoryTheory.SemiCartesianMonoidalCategory.comp_toUnit_assoc CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unit CategoryTheory.Category.id_comp CategoryTheory.GrpObj.lift_comp_inv_right pointOfClosedPoint_apply CategoryTheory.CommaMorphism.w locallyOfFinitePresentation_comp locallyOfFinitePresentation_of_isOpenImmersion IsOpenImmersion.of_isIso CategoryTheory.Comma.instIsIsoLeft CategoryTheory.Iso.isIso_hom Mathlib.Tactic.DepRewrite.nddcongrArg Scheme.Hom.preimage_smoothLocus_eq Scheme.Hom.mem_preimage

---

← Back to Index