Theorem AlgebraicGeometry.IsSmoothOfRelativeDimension.isSmooth

Modification history

2026-02-09 16:00
Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean
chore(AlgebraicGeometry/Smooth): rename `IsSmooth` to `Smooth` and `IsEtale` to `Etale` (#35028) …
Deleted AlgebraicGeometry.IsSmoothOfRelativeDimension.isSmoothView on Github →
2024-10-17 09:39
Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean
feat(AlgebraicGeometry): smooth morphisms of schemes (#14161) …
Added AlgebraicGeometry.IsSmoothOfRelativeDimension.isSmoothView on Github →