Theorem AlgebraicGeometry.RingedSpace.basicOpen_of_isUnit

Modification history

2023-06-02 12:18
Mathlib/AlgebraicGeometry/RingedSpace.lean
feat: port AlgebraicGeometry.RingedSpace (#4499)
Added AlgebraicGeometry.RingedSpace.basicOpen_of_isUnitView on Github →