Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prime_spectrum.mem_compl_zero_locus_iff_not_mem

Modification history

2021-01-20 09:51
src/algebraic_geometry/prime_spectrum.lean
feat(algebraic_geometry/is_open_comap_C): add file is_open_comap_C, prove that Spec R[x] \to Spec R is an open map (#5693) …
Added prime_spectrum.mem_compl_zero_locus_iff_not_memView on Github →