Def AlgebraicGeometry.Proj.openCoverOfISupEqTop

Modification history

2025-10-02 14:13

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

chore(Mathlib/AlgebraicGeometry/Restrict): change openCoverOfISupEqTop to openCoverOfIsOpenCover (#30072) …

Deleted AlgebraicGeometry.Proj.openCoverOfISupEqTop View on Github →

2024-11-17 17:51

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

feat(AlgebraicGeometry): basic API for `Proj` (#19152)

Added AlgebraicGeometry.Proj.openCoverOfISupEqTop View on Github →