Theorem AlgebraicGeometry.SmoothOfRelativeDimension.smooth

Modification history

2026-02-10 11:38
Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean
refactor(AlgebraicGeometry/Smooth): replace `Locally IsStandardSmooth` by `Smooth` (#35034) …
Modified AlgebraicGeometry.SmoothOfRelativeDimension.smoothView 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.SmoothOfRelativeDimension.smoothView on Github →