Theorem AlgebraicGeometry.smooth_isStableUnderBaseChange

Modification history

2026-02-10 11:38

Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

refactor(AlgebraicGeometry/Smooth): replace `Locally IsStandardSmooth` by `Smooth` (#35034) …

Deleted AlgebraicGeometry.smooth_isStableUnderBaseChange View on Github →

2026-02-09 16:00

Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean

chore(AlgebraicGeometry/Smooth): rename `IsSmooth` to `Smooth` and `IsEtale` to `Etale` (#35028) …

Added AlgebraicGeometry.smooth_isStableUnderBaseChange View on Github →