Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-25 09:58 b599b58c

View on Github →

refactor(algebraic_geometry/*): Tidy up simp lemmas regarding basic_opens. (#17014)

Estimated changes

Modified src/algebraic_geometry/AffineScheme.lean

added theorem algebraic_geometry.exists_basic_open_le_affine_inter

deleted theorem algebraic_geometry.exists_basic_open_subset_affine_inter

added theorem algebraic_geometry.is_affine_open.exists_basic_open_le

deleted theorem algebraic_geometry.is_affine_open.exists_basic_open_subset

Modified src/algebraic_geometry/Scheme.lean

added theorem algebraic_geometry.Scheme.basic_open_le

deleted theorem algebraic_geometry.Scheme.basic_open_subset

modified theorem algebraic_geometry.Scheme.basic_open_zero

Modified src/algebraic_geometry/locally_ringed_space.lean

Modified src/algebraic_geometry/locally_ringed_space/has_colimits.lean

Modified src/algebraic_geometry/morphisms/quasi_compact.lean

Modified src/algebraic_geometry/morphisms/ring_hom_properties.lean

Modified src/algebraic_geometry/open_immersion.lean

Modified src/algebraic_geometry/prime_spectrum/basic.lean

Modified src/algebraic_geometry/properties.lean

deleted theorem algebraic_geometry.eq_zero_of_basic_open_empty

added theorem algebraic_geometry.eq_zero_of_basic_open_eq_bot

Modified src/algebraic_geometry/ringed_space.lean

added theorem algebraic_geometry.RingedSpace.basic_open_le

deleted theorem algebraic_geometry.RingedSpace.basic_open_subset