Theorem AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth

Modification history

2026-02-10 11:38
Mathlib/AlgebraicGeometry/Morphisms/Smooth.lean
refactor(AlgebraicGeometry/Smooth): replace `Locally IsStandardSmooth` by `Smooth` (#35034) …
Added AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmoothView on Github →