Theorem PrimeSpectrum.primeSpectrumProd_symm_inr

Modification history

2024-07-12 14:35

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

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

Added PrimeSpectrum.primeSpectrumProd_symm_inr View on Github →