Theorem: Ideal.ker_Pi_Quotient_mk (GlimpseOfLean/Solutions/Topics/ChineseRemainder.lean)

State before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : ι → Ideal R
⊢ ker (Pi.ringHom fun i => Quotient.mk (I i)) = ⨅ i, I i
Tactic:
simp [Pi.ker_ringHom, Ideal.ker_mk]
State after:
no goals