Theorem: chineseMap_inj (LeanCourse/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:
sorry
State after:
no goals