Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-23 12:54 f3b380e4

View on Github →

feat(algebraic_geometry): Prime spectrum is sober. (#10989)

Estimated changes

Modified src/algebraic_geometry/prime_spectrum/basic.lean

added theorem prime_spectrum.is_closed_iff_zero_locus_ideal

added theorem prime_spectrum.is_closed_iff_zero_locus_radical_ideal

added theorem prime_spectrum.is_irreducible_zero_locus_iff

added theorem prime_spectrum.is_irreducible_zero_locus_iff_of_radical

Modified src/topology/sober.lean

added theorem is_generic_point_iff_forall_closed

Modified src/topology/subset_properties.lean

added theorem irreducible_space_def