Mathlib v3 is deprecated. Go to Mathlib v4

Def algebraic_geometry.RingedSpace

Modification history

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.RingedSpaceView on Github →