Mathlib Changelog
v3
Changelog
About
Github
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