Commit 2024-07-12 14:35 6bfe732c

View on Github →

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

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added def PrimeSpectrum.primeSpectrumProdHomeo

added theorem PrimeSpectrum.primeSpectrumProd_symm_inl

added theorem PrimeSpectrum.primeSpectrumProd_symm_inr

Modified Mathlib/Topology/Constructions.lean

added theorem isClosedMap_sum