Mathlib v3 is deprecated. Go to Mathlib v4

Def prime_spectrum.prime_spectrum_prod_of_sum

Modification history

2022-11-26 13:40

src/algebraic_geometry/prime_spectrum/basic.lean

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

Added prime_spectrum.prime_spectrum_prod_of_sum View on Github →