Commit 2026-02-09 16:00 d1366e1a

View on Github →

chore(AlgebraicGeometry/Smooth): rename IsSmooth to Smooth and IsEtale to Etale (#35028) This way it matches Algebra.Smooth and Algebra.Etale. Also there is no possible confusion, because these are clearly adjectives.

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Etale.lean

added theorem AlgebraicGeometry.Etale.of_comp

deleted theorem AlgebraicGeometry.IsEtale.of_comp

deleted def AlgebraicGeometry.Scheme.Etale

Modified Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

deleted theorem AlgebraicGeometry.IsSmoothOfRelativeDimension.isSmooth

added theorem AlgebraicGeometry.SmoothOfRelativeDimension.smooth

deleted theorem AlgebraicGeometry.isSmoothOfRelativeDimension_isStableUnderBaseChange

deleted theorem AlgebraicGeometry.isSmooth_isStableUnderBaseChange

added theorem AlgebraicGeometry.smoothOfRelativeDimension_isStableUnderBaseChange

added theorem AlgebraicGeometry.smooth_isStableUnderBaseChange

Modified Mathlib/AlgebraicGeometry/Sites/Etale.lean