R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ Multiset.sum (Multiset.map (fun i => nextCoeff (X - ↑C i)) t) = -Multiset.sum t

case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ ∀ (i : R), i ∈ t → Monic (X - ↑C i)
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ nextCoeff (prod (Multiset.map (fun x => X - ↑C x) t)) = -Multiset.sum t
rw [nextCoeff_multiset_prod]
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ Multiset.sum (Multiset.map (fun x => -x) t) = -Multiset.sum t
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ Multiset.sum (Multiset.map (fun i => nextCoeff (X - ↑C i)) t) = -Multiset.sum t
simp only [nextCoeff_X_sub_C]
no goals
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ Multiset.sum (Multiset.map (fun x => -x) t) = -Multiset.sum t
exact t.sum_hom (-AddMonoidHom.id R)
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
i✝ : R
a✝ : i✝ ∈ t
⊢ Monic (X - ↑C i✝)
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
⊢ ∀ (i : R), i ∈ t → Monic (X - ↑C i)
intros
no goals
case h
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommRing R
t : Multiset R
i✝ : R
a✝ : i✝ ∈ t
⊢ Monic (X - ↑C i✝)
apply monic_X_sub_C