Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.LocallyRingedSpace.basic_open_zero

Modification history

2021-12-27 16:46

src/algebraic_geometry/locally_ringed_space.lean

feat(algebraic_geometry): Basic open set is empty iff section is zero in reduced schemes. (#11012)

Added algebraic_geometry.LocallyRingedSpace.basic_open_zero View on Github →