Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebraic_geometry.RingedSpace.is_unit_res_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.is_unit_res_basic_open View 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.is_unit_res_basic_open View on Github →