Mathlib v3 is deprecated. Go to Mathlib v4

Def algebraic_geometry.RingedSpace.basic_open

Modification history

2021-11-30 11:49
src/algebraic_geometry/ringed_space.lean
feat(algebraic_geometry): Generalized basic open for arbitrary sections (#10515)
Modified algebraic_geometry.RingedSpace.basic_openView on Github →
2021-10-01 08:55
src/algebraic_geometry/ringed_space.lean
feat(algebraic_geometry/ringed_space): Define basic opens for ringed spaces. (#9358) …
Added algebraic_geometry.RingedSpace.basic_openView on Github →