R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.417705
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ IsClosed (zeroLocus ↑(ker f))
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.417705
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ IsClosed (Set.range ↑(comap f))
rw [range_comap_of_surjective _ f hf]
no goals
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.417705
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ IsClosed (zeroLocus ↑(ker f))
exact isClosed_zeroLocus _