Commit 2026-03-10 20:55 e13110e9

View on Github →

feat(AlgebraicGeometry): intersection of affine opens in separated schemes is affine (#36453)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

added theorem AlgebraicGeometry.IsAffineOpen.biInf

added theorem AlgebraicGeometry.IsAffineOpen.iInf

added theorem AlgebraicGeometry.IsAffineOpen.inf

added theorem AlgebraicGeometry.diagonal_isAffine_iff_forall_isAffineOpen_inf

added theorem AlgebraicGeometry.isAffineHom_diagonal_iff