Theorem: chineseMap_inj (MIL/C08_Groups_and_Rings/S02_Rings.lean)

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