Def AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan

Modification history

2025-10-07 11:23

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

chore: Rename Proj.openCoverOfIsOpenCover to Proj.affineOpenCoverOfIrrelevantLESpan (#30288) …

Added AlgebraicGeometry.Proj.affineOpenCoverOfIrrelevantLESpan View on Github →