case h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus ↑(Ideal.span s) ↔ x ∈ zeroLocus s
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
⊢ zeroLocus ↑(Ideal.span s) = zeroLocus s
ext x
no goals
case h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus ↑(Ideal.span s) ↔ x ∈ zeroLocus s
exact (Submodule.gi R R).gc s x.asIdeal