Theorem AlgebraicGeometry.Scheme.IsQuasiAffine.of_forall_exists_mem_basicOpen

Modification history

2025-10-25 17:18
Mathlib/AlgebraicGeometry/QuasiAffine.lean
feat(AlgebraicGeometry): quasi-affine if covered by affine basic opens of global sections (#30286)
Added AlgebraicGeometry.Scheme.IsQuasiAffine.of_forall_exists_mem_basicOpenView on Github →