Def PrimeSpectrum.primeSpectrumProdHomeo

Modification history

2024-07-12 14:35

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

feat(AlgebraicGeometry/PrimeSpectrum): Prime spectrum of products of rings. (#14550)

Added PrimeSpectrum.primeSpectrumProdHomeo View on Github →