R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s) ∪ zeroLocus ↑(Ideal.span s')
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s ⊓ Ideal.span s')
rw [zeroLocus_inf]
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s) ∪ zeroLocus ↑(Ideal.span s')
simp