LocallyStandardSmooth

📁 Source: Mathlib/RingTheory/RingHom/LocallyStandardSmooth.lean

Statistics

Metric	Count
Definitions	0
Theorems smooth, locally_isStandardSmooth, etale_iff_isStandardSmoothOfRelativeDimension_zero, smooth_iff_locally_isStandardSmooth	4
Total	4

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
etale_iff_isStandardSmoothOfRelativeDimension_zero 📖	mathematical	—	Etale IsStandardSmoothOfRelativeDimension	—	Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero
smooth_iff_locally_isStandardSmooth 📖	mathematical	—	Smooth Locally IsStandardSmooth	—	Smooth.locally_isStandardSmooth locally_iff_of_localizationSpanTarget PropertyIsLocal.respectsIso Smooth.propertyIsLocal Smooth.ofLocalizationSpanTarget locally_of_locally IsStandardSmooth.smooth

RingHom.IsStandardSmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smooth 📖	mathematical	—	RingHom.Smooth	—	RingHom.Smooth.eq_1 Algebra.instSmoothOfIsStandardSmooth toAlgebra

RingHom.Smooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locally_isStandardSmooth 📖	mathematical	—	RingHom.Locally RingHom.IsStandardSmooth	—	Algebra.Smooth.exists_span_eq_top_isStandardSmooth toAlgebra RingHom.algebraMap_toAlgebra IsScalarTower.algebraMap_eq OreLocalization.instIsScalarTower IsScalarTower.right RingHom.isStandardSmooth_algebraMap

---

← Back to Index