Commit 2025-10-02 14:13 f5bc8795

View on Github →

chore(Mathlib/AlgebraicGeometry/Restrict): change openCoverOfISupEqTop to openCoverOfIsOpenCover (#30072) This PR changes AlgebraicGeometry.Scheme.openCoverOfISupEqTop into AlgebraicGeometry.Scheme.openCoverOfISupEqTop, which now takes TopologicalSpace.IsOpenCover.

Estimated changes

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

deleted def AlgebraicGeometry.Proj.openCoverOfISupEqTop

added def AlgebraicGeometry.Proj.openCoverOfIsOpenCover

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean

Modified Mathlib/AlgebraicGeometry/Restrict.lean

deleted def AlgebraicGeometry.Scheme.openCoverOfISupEqTop

added def AlgebraicGeometry.Scheme.openCoverOfIsOpenCover