Theorem AlgebraicGeometry.exists_basicOpen_le_appLE_of_appLE_of_isAffine

Modification history

2024-10-17 09:39
Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
feat(AlgebraicGeometry): smooth morphisms of schemes (#14161) …
Added AlgebraicGeometry.exists_basicOpen_le_appLE_of_appLE_of_isAffineView on Github →