Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-30 11:49 1077f346

View on Github →

feat(algebraic_geometry): Generalized basic open for arbitrary sections (#10515)

Estimated changes

Modified src/algebraic_geometry/locally_ringed_space.lean

added theorem algebraic_geometry.LocallyRingedSpace.preimage_basic_open

Modified src/algebraic_geometry/ringed_space.lean

modified def algebraic_geometry.RingedSpace.basic_open

added theorem algebraic_geometry.RingedSpace.basic_open_res

added theorem algebraic_geometry.RingedSpace.basic_open_subset

modified theorem algebraic_geometry.RingedSpace.is_unit_res_basic_open

modified theorem algebraic_geometry.RingedSpace.mem_basic_open