Def AlgebraicGeometry.Proj.openCoverOfIsOpenCover

Modification history

2025-10-07 11:23
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
chore: Rename Proj.openCoverOfIsOpenCover to Proj.affineOpenCoverOfIrrelevantLESpan (#30288) …
Deleted AlgebraicGeometry.Proj.openCoverOfIsOpenCoverView on Github →
2025-10-02 14:13
Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
chore(Mathlib/AlgebraicGeometry/Restrict): change openCoverOfISupEqTop to openCoverOfIsOpenCover (#30072) …
Added AlgebraicGeometry.Proj.openCoverOfIsOpenCoverView on Github →