R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) a = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0
intro a ha
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) (sum a fun n a => ↑(monomial n) a) = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) a = 0
rw [← sum_monomial_eq a]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X (sum a fun n a => ↑(monomial n) a) = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) (sum a fun n a => ↑(monomial n) a) = 0
dsimp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (sum a fun n a => eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) a)) = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X (sum a fun n a => ↑(monomial n) a) = 0
rw [eval₂_sum]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ (fun n a => eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) a)) n (coeff a n) = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (sum a fun n a => eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) a)) = 0
refine' Finset.sum_eq_zero fun n _ => _
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) (coeff a n)) = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ (fun n a => eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) a)) n (coeff a n) = 0
dsimp
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ ↑(RingHom.comp C (Quotient.mk I)) (coeff a n) * X ^ n = 0
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) (coeff a n)) = 0
rw [eval₂_monomial (C.comp (Quotient.mk I)) X]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
⊢ coeff (↑(RingHom.comp C (Quotient.mk I)) (coeff a n)) m = coeff 0 m
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ ↑(RingHom.comp C (Quotient.mk I)) (coeff a n) * X ^ n = 0
refine' mul_eq_zero_of_left (Polynomial.ext fun m => _) (X ^ n)
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
⊢ coeff (↑(RingHom.comp C (Quotient.mk I)) (coeff a n)) m = coeff 0 m
erw [coeff_C]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
h : m = 0
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m

case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
h : ¬m = 0
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
by_cases h : m = 0
no goals
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
h : m = 0
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
simpa [h] using Quotient.eq_zero_iff_mem.2 ((mem_map_C_iff.1 ha) n)
no goals
case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
h : ¬m = 0
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
simp [h]