Theorems · Theorem · commutative algebra

PrimeSpectrum.toPiLocalization_not_surjective_of_infinite

∀ {ι : Type u_5} (R : ι → Type u_4) [inst : (i : ι) → CommSemiring (R i)] [∀ (i : ι), Nontrivial (R i)] [Infinite ι],
  ¬Function.Surjective ⇑(PrimeSpectrum.toPiLocalization ((i : ι) → R i))

Defined in

Mathlib.RingTheory.Spectrum.Maximal.Localization

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringNontrivialInfinite