Theorems · Theorem · algebraic geometry

PrimeSpectrum.sigmaToPi_mk_basicOpen

∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → CommRing (R i)] [inst_1 : DecidableEq ι] (i : ι) (f : R i),
  PrimeSpectrum.sigmaToPi R '' Sigma.mk i '' ↑(PrimeSpectrum.basicOpen f) = ↑(PrimeSpectrum.basicOpen (Pi.single i f))

Defined in

Mathlib.RingTheory.Spectrum.Prime.Topology

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingDecidableEq