Theorems · Theorem · algebraic geometry

AlgebraicGeometry.coprodSpec_coprodMk

∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S]
  (x : ↥(AlgebraicGeometry.Spec (CommRingCat.of R)) ⊕ ↥(AlgebraicGeometry.Spec (CommRingCat.of S))),
  (AlgebraicGeometry.coprodSpec R S)
      ((AlgebraicGeometry.coprodMk (AlgebraicGeometry.Spec (CommRingCat.of R))
          (AlgebraicGeometry.Spec (CommRingCat.of S)))
        x) =
    (PrimeSpectrum.primeSpectrumProd R S).symm x

Defined in

Mathlib.AlgebraicGeometry.Limits

Cited by

1 results in Mathlib

Foundations

Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRing