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
⊢ coeff (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots P))) 0 = (-1) ^ natDegree P * Multiset.prod (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
⊢ coeff P 0 = (-1) ^ natDegree P * Multiset.prod (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.prod (Multiset.map (eval 0 ∘ fun a => X - ↑C a) (roots P)) = (-1) ^ natDegree P * Multiset.prod (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
⊢ coeff (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots P))) 0 = (-1) ^ natDegree P * Multiset.prod (roots P)
rw [coeff_zero_eq_eval_zero, eval_multiset_prod, Multiset.map_map]
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.prod (Multiset.map (fun x => -x) (roots P)) = (-1) ^ natDegree P * Multiset.prod (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
⊢ Multiset.prod (Multiset.map (eval 0 ∘ fun a => X - ↑C a) (roots P)) = (-1) ^ natDegree P * Multiset.prod (roots P)
simp_rw [Function.comp_apply, eval_sub, eval_X, zero_sub, eval_C]
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.prod (Multiset.map (fun x => -1 * x) (roots P)) = (-1) ^ natDegree P * Multiset.prod (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
⊢ Multiset.prod (Multiset.map (fun x => -x) (roots P)) = (-1) ^ natDegree P * Multiset.prod (roots P)
conv_lhs =>
  congr
  congr
  ext
  rw [neg_eq_neg_one_mul]
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.prod (Multiset.map (fun x => -1 * x) (roots P)) = (-1) ^ natDegree P * Multiset.prod (roots P)
simp only [splits_iff_card_roots.1 hP, neg_mul, one_mul, Multiset.prod_map_neg]