Theorems · Theorem · algebraic geometry
PrimeSpectrum.comap_evalRingHom_basicOpen
∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → CommRing (R i)] [inst_1 : DecidableEq ι] (i : ι) (f : R i),
PrimeSpectrum.comap (Pi.evalRingHom R i) '' ↑(PrimeSpectrum.basicOpen f) = ↑(PrimeSpectrum.basicOpen (Pi.single i f))- Cited by
- 2 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites29
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- SetLike.coestatement and proof · cited by 8,199
- Set.imagestatement and proof · cited by 5,609
- Set.rangeproof · cited by 4,705
- Set.extproof · cited by 2,266
- MulZeroClass.mul_zeroproof · cited by 2,091
- TopologicalSpace.Opensstatement · cited by 2,040
- MulZeroClass.zero_mulproof · cited by 1,625
- PrimeSpectrumstatement and proof · cited by 625
- Pi.singlestatement and proof · cited by 518
- RingHom.kerproof · cited by 363
Cited by2
Results whose statement or proof uses this declaration.
- PrimeSpectrum.isOpenEmbedding_sigmaToPiproof · cited by 0
- PrimeSpectrum.sigmaToPi_mk_basicOpenproof · cited by 0