Theorems · Theorem · algebraic geometry

PrimeSpectrum.isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton

∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {f : R}
  {p : PrimeSpectrum R},
  (PrimeSpectrum.basicOpen f).carrier = {p} → (IsLocalization.Away f S ↔ IsLocalization.AtPrime S p.asIdeal)

Defined in

Mathlib.RingTheory.Spectrum.Prime.Topology

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebra