Theorems · Theorem · algebraic geometry

PrimeSpectrum.toPiLocalizationEquiv_apply

∀ (R : Type u) [inst : CommSemiring R] [inst_1 : DiscreteTopology (PrimeSpectrum R)] (x : R),
  (PrimeSpectrum.toPiLocalizationEquiv R) x = (algebraMap R (PrimeSpectrum.PiLocalization R)) x

Defined in

Mathlib.RingTheory.Spectrum.Prime.Topology

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringDiscreteTopology