ext x
R : Type u_1
S : Type ?u.14649
inst✝¹ : CommRing R
ι : Type ?u.14646
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker (Quotient.mk I) = I
case h
R : Type u_1
S : Type ?u.14649
inst✝¹ : CommRing R
ι : Type ?u.14646
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ a ∈ I, f a = 0
x : R
⊢ x ∈ ker (Quotient.mk I) ↔ x ∈ I