Theorem AlgebraicGeometry.diagonal_isAffine_iff_forall_isAffineOpen_inf

Modification history

2026-03-10 20:55
Mathlib/AlgebraicGeometry/Morphisms/Affine.lean
feat(AlgebraicGeometry): intersection of affine opens in separated schemes is affine (#36453)
Added AlgebraicGeometry.diagonal_isAffine_iff_forall_isAffineOpen_infView on Github →