Commit 2024-04-12 14:33 eb0a213d

View on Github →

feat(AlgebraicGeometry/OpenImmersion): Affine open covers, and refinements of open covers by affine ones (#11947)

Estimated changes

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

added def AlgebraicGeometry.Scheme.AffineOpenCover.openCover

added structure AlgebraicGeometry.Scheme.AffineOpenCover

added def AlgebraicGeometry.Scheme.OpenCover.affineRefinement

added def AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement

added def AlgebraicGeometry.Scheme.affineOpenCover

added theorem AlgebraicGeometry.Scheme.openCover_affineOpenCover