F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ nextCoeff (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots P))) = -Multiset.sum (roots P)
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ nextCoeff P = -Multiset.sum (roots P)
nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ Multiset.sum (Multiset.map (fun i => nextCoeff (X - ↑C i)) (roots P)) = -Multiset.sum (roots P)

F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ ∀ (a : K), a ∈ roots P → Monic (X - ↑C a)
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ nextCoeff (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots P))) = -Multiset.sum (roots P)
rw [Monic.nextCoeff_multiset_prod _ _ fun a ha => _]
no goals
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ Multiset.sum (Multiset.map (fun i => nextCoeff (X - ↑C i)) (roots P)) = -Multiset.sum (roots P)
simp_rw [nextCoeff_X_sub_C, Multiset.sum_map_neg']
no goals
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
P : K[X]
hmo : Monic P
hP : Splits (RingHom.id K) P
⊢ ∀ (a : K), a ∈ roots P → Monic (X - ↑C a)
simp only [monic_X_sub_C, implies_true]