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

State before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : ι → Ideal R
⊢ Injective ⇑(chineseMap I)
Tactic:
rw [chineseMap, injective_lift_iff, ker_Pi_Quotient_mk]
State after:
no goals