R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (PrimeSpectrum R)
⊢ Ideal.IsRadical (Ideal.radical (vanishingIdeal s))
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (PrimeSpectrum R)
⊢ Ideal.IsRadical (vanishingIdeal s)
rw [← vanishingIdeal_closure, ← zeroLocus_vanishingIdeal_eq_closure,
  vanishingIdeal_zeroLocus_eq_radical]
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (PrimeSpectrum R)
⊢ Ideal.IsRadical (Ideal.radical (vanishingIdeal s))
apply Ideal.radical_isRadical