R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
⊢ zeroLocus {f}ᶜ = ↑⊥ ↔ IsNilpotent f
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
⊢ basicOpen f = ⊥ ↔ IsNilpotent f
rw [← TopologicalSpace.Opens.coe_inj, basicOpen_eq_zeroLocus_compl]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
⊢ (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), Ideal.IsPrime J → f ∈ J
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
⊢ zeroLocus {f}ᶜ = ↑⊥ ↔ IsNilpotent f
simp only [Set.eq_univ_iff_forall, Set.singleton_subset_iff, TopologicalSpace.Opens.coe_bot,
  nilpotent_iff_mem_prime, Set.compl_empty_iff, mem_zeroLocus, SetLike.mem_coe]
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
⊢ (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), Ideal.IsPrime J → f ∈ J
exact ⟨fun h I hI => h ⟨I, hI⟩, fun h ⟨I, hI⟩ => h I hI⟩