R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
f : R
⊢ (∀ (x : PrimeSpectrum R), x ∈ zeroLocus ↑I → f ∈ x.asIdeal) ↔
    ∀ (p : Submodule R R), p ∈ {J | I ≤ J ∧ Ideal.IsPrime J} → f ∈ p
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
f : R
⊢ f ∈ vanishingIdeal (zeroLocus ↑I) ↔ f ∈ Ideal.radical I
rw [mem_vanishingIdeal, Ideal.radical_eq_sInf, Submodule.mem_sInf]
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
f : R
⊢ (∀ (x : PrimeSpectrum R), x ∈ zeroLocus ↑I → f ∈ x.asIdeal) ↔
    ∀ (p : Submodule R R), p ∈ {J | I ≤ J ∧ Ideal.IsPrime J} → f ∈ p
exact ⟨fun h x hx => h ⟨x, hx.2⟩ hx.1, fun h x hx => h x.1 ⟨hx, x.2⟩⟩