R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
⊢ ∃ s_1, zeroLocus s = zeroLocus s_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
⊢ IsClosed (zeroLocus s)
rw [isClosed_iff_zeroLocus]
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
⊢ ∃ s_1, zeroLocus s = zeroLocus s_1
exact ⟨s, rfl⟩