Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-27 16:46 a3603547

View on Github →

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

Estimated changes

Modified src/algebraic_geometry/locally_ringed_space.lean

added theorem algebraic_geometry.LocallyRingedSpace.basic_open_zero

Modified src/algebraic_geometry/prime_spectrum/basic.lean

added theorem prime_spectrum.basic_open_eq_bot_iff

Modified src/algebraic_geometry/properties.lean

added theorem algebraic_geometry.basic_open_eq_bot_iff

added theorem algebraic_geometry.basic_open_eq_of_affine'

added theorem algebraic_geometry.basic_open_eq_of_affine

added theorem algebraic_geometry.eq_zero_of_basic_open_empty

added theorem algebraic_geometry.is_reduced_of_open_immersion

added theorem algebraic_geometry.reduce_to_affine_global

Modified src/algebraic_geometry/structure_sheaf.lean

Modified src/ring_theory/nilpotent.lean

added theorem is_reduced_of_injective

Modified src/topology/opens.lean

added theorem topological_space.opens.coe_bot