Theorem: chineseMap_inj (LeanCourse/MIL/C08_Groups_and_Rings/solutions/Solutions_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