R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
I : PrimeSpectrum R
⊢ ¬f ∈ ↑I.asIdeal ↔ ¬f ∈ I.asIdeal
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
I : PrimeSpectrum R
⊢ I ∈ zeroLocus {f}ᶜ ↔ ¬f ∈ I.asIdeal
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
I : PrimeSpectrum R
⊢ ¬f ∈ ↑I.asIdeal ↔ ¬f ∈ I.asIdeal
rfl