Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-21 11:26 bb7631fb

View on Github →

feat(algebraic_geometry/prime_spectrum): vanishing ideal (#1972)

wip
wip
Remove stuff for next PR
Update prime_spectrum.lean
Process comments

Estimated changes

Modified src/algebraic_geometry/prime_spectrum.lean

deleted theorem prime_spectrum.Inter_zero_locus

added theorem prime_spectrum.coe_vanishing_ideal

added theorem prime_spectrum.gc

added theorem prime_spectrum.gc_set

added theorem prime_spectrum.is_closed_zero_locus

added theorem prime_spectrum.le_vanishing_ideal_zero_locus

added theorem prime_spectrum.mem_vanishing_ideal

added theorem prime_spectrum.subset_vanishing_ideal_zero_locus

added theorem prime_spectrum.subset_zero_locus_iff_le_vanishing_ideal

added theorem prime_spectrum.subset_zero_locus_iff_subset_vanishing_ideal

added theorem prime_spectrum.subset_zero_locus_vanishing_ideal

added theorem prime_spectrum.sup_vanishing_ideal_le

modified theorem prime_spectrum.union_zero_locus

deleted theorem prime_spectrum.union_zero_locus_ideal

added def prime_spectrum.vanishing_ideal

added theorem prime_spectrum.vanishing_ideal_Union

added theorem prime_spectrum.vanishing_ideal_union

added theorem prime_spectrum.vanishing_ideal_univ

modified theorem prime_spectrum.zero_locus_Union

added theorem prime_spectrum.zero_locus_bot

added theorem prime_spectrum.zero_locus_empty

added theorem prime_spectrum.zero_locus_empty_iff_eq_top

added theorem prime_spectrum.zero_locus_inf

deleted theorem prime_spectrum.zero_locus_is_closed

added theorem prime_spectrum.zero_locus_sup

added theorem prime_spectrum.zero_locus_supr

added theorem prime_spectrum.zero_locus_union

added theorem prime_spectrum.zero_locus_vanishing_ideal_eq_closure