Theorems · Theorem · algebraic geometry

MaximalSpectrum.toPiLocalizationEquiv_apply_apply

∀ (R : Type u) [inst : CommSemiring R] [inst_1 : DiscreteTopology (PrimeSpectrum R)] (x : R) (I : MaximalSpectrum R),
  (MaximalSpectrum.toPiLocalizationEquiv R) x I = (algebraMap R (Localization.AtPrime I.asIdeal)) x

Defined in

Mathlib.RingTheory.Spectrum.Prime.Topology

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringDiscreteTopology