feat(field_theory/splitting_field): add eval_root_derivative_of_split (…

…#10224)

From flt-regular.

src/data/polynomial/derivative.lean

@@ -237,6 +237,27 @@ polynomial.induction_on p
       @derivative_mul _ _ _ X, derivative_X, mul_one, eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X,
       add_mul, mul_right_comm])
 
+theorem derivative_prod {s : multiset ι} {f : ι → polynomial R} :
+  (multiset.map f s).prod.derivative =
+  (multiset.map (λ i, (multiset.map f (s.erase i)).prod * (f i).derivative) s).sum :=
+begin
+  refine multiset.induction_on s (by simp) (λ i s h, _),
+  rw [multiset.map_cons, multiset.prod_cons, derivative_mul, multiset.map_cons _ i s,
+    multiset.sum_cons, multiset.erase_cons_head, mul_comm (f i).derivative],
+  congr,
+  rw [h, ← add_monoid_hom.coe_mul_left, (add_monoid_hom.mul_left (f i)).map_multiset_sum _,
+    add_monoid_hom.coe_mul_left],
+  simp only [function.comp_app, multiset.map_map],
+  congr' 1,
+  refine multiset.map_congr (λ j hj, _),
+  simp only [function.comp_app],
+  rw [← mul_assoc, ← multiset.prod_cons, ← multiset.map_cons],
+  congr' 1,
+  by_cases hij : i = j,
+  { simp [hij, ← multiset.prod_cons, ← multiset.map_cons, multiset.cons_erase hj] },
+  { simp [hij] }
+end
+
 theorem of_mem_support_derivative {p : polynomial R} {n : ℕ} (h : n ∈ p.derivative.support) :
   n + 1 ∈ p.support :=
 mem_support_iff.2 $ λ (h1 : p.coeff (n+1) = 0), mem_support_iff.1 h $
@@ -301,6 +322,14 @@ begin
   { simp [ih p.derivative, iterate_derivative_neg, derivative_comp, pow_succ], },
 end
 
+lemma eval_multiset_prod_X_sub_C_derivative {S : multiset R} {r : R} (hr : r ∈ S) :
+  eval r (multiset.map (λ a, X - C a) S).prod.derivative =
+  (multiset.map (λ a, r - a) (S.erase r)).prod :=
+begin
+  nth_rewrite 0 [← multiset.cons_erase hr],
+  simpa using (eval_ring_hom r).map_multiset_prod (multiset.map (λ a, X - C a) (S.erase r)),
+end
+
 end comm_ring
 
 section is_domain

src/field_theory/splitting_field.lean

@@ -437,6 +437,18 @@ begin
     exact (C_leading_coeff_mul_prod_multiset_X_sub_C hroots).symm },
 end
 
+lemma aeval_root_derivative_of_splits [algebra K L] {P : polynomial K} (hmo : P.monic)
+  (hP : P.splits (algebra_map K L)) {r : L} (hr : r ∈ (P.map (algebra_map K L)).roots) :
+  aeval r P.derivative =
+  (multiset.map (λ a, r - a) ((P.map (algebra_map K L)).roots.erase r)).prod :=
+begin
+  replace hmo := monic_map (algebra_map K L) hmo,
+  replace hP := (splits_id_iff_splits (algebra_map K L)).2 hP,
+  rw [aeval_def, ← eval_map, ← derivative_map],
+  nth_rewrite 0 [eq_prod_roots_of_monic_of_splits_id hmo hP],
+  rw [eval_multiset_prod_X_sub_C_derivative hr]
+end
+
 end splits
 
 end polynomial