R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
i : R
hi : i ∈ I
⊢ ↑C i ∈ Ideal.map C I
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
i : R
hi : i ∈ I
⊢ ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.Quotient.eq_zero_iff_mem]
no goals
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
i : R
hi : i ∈ I
⊢ ↑C i ∈ Ideal.map C I
exact Ideal.mem_map_of_mem _ hi