Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-26 13:40 052f6013

View on Github →

refactor(algebraic_geometry/prime_spectrum/basic): refactor prime_spectrum def into structure (#16930)

Estimated changes

Modified src/algebraic_geometry/prime_spectrum/basic.lean

modified def local_ring.closed_point

deleted def prime_spectrum.as_ideal

modified theorem prime_spectrum.as_ideal_le_as_ideal

modified theorem prime_spectrum.as_ideal_lt_as_ideal

deleted theorem prime_spectrum.ext

added def prime_spectrum.prime_spectrum_prod_of_sum

added structure prime_spectrum

deleted def prime_spectrum

Modified src/algebraic_geometry/prime_spectrum/is_open_comap_C.lean

Modified src/algebraic_geometry/prime_spectrum/maximal.lean

Modified src/algebraic_geometry/prime_spectrum/noetherian.lean

Modified src/ring_theory/dedekind_domain/ideal.lean

Modified src/ring_theory/ideal/prod.lean

deleted theorem ideal.prime_ideals_equiv_symm_inl

deleted theorem ideal.prime_ideals_equiv_symm_inr

Modified src/ring_theory/valuation/valuation_subring.lean