R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) (Finset.sum (support a) fun v => ↑(monomial v) (coeff v a)) = 0
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0
rw [as_sum a]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ (Finset.sum (support a) fun x => eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X (↑(monomial x) (coeff x a))) = 0
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) (Finset.sum (support a) fun v => ↑(monomial v) (coeff v a)) = 0
rw [coe_eval₂Hom, eval₂_sum]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X (↑(monomial n) (coeff n a)) = 0
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ (Finset.sum (support a) fun x => eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X (↑(monomial x) (coeff x a))) = 0
refine' Finset.sum_eq_zero fun n _ => _
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ (↑C (↑(Ideal.Quotient.mk I) (coeff n a)) * Finsupp.prod n fun n e => X n ^ e) = 0
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X (↑(monomial n) (coeff n a)) = 0
simp only [eval₂_monomial, Function.comp_apply, RingHom.coe_comp]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ (↑C (↑(Ideal.Quotient.mk I) (coeff n a)) * Finsupp.prod n fun n e => X n ^ e) = 0
refine' mul_eq_zero_of_left _ _
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ coeff n a ∈ I
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
suffices coeff n a ∈ I by
  rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this
  simp only [this, C_0]
no goals
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ coeff n a ∈ I
exact mem_map_C_iff.1 ha n
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
this : ↑(Ideal.Quotient.mk I) (coeff n a) = 0
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
this : coeff n a ∈ I
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this
no goals
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
this : ↑(Ideal.Quotient.mk I) (coeff n a) = 0
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
simp only [this, C_0]