F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
hP : Splits (algebraMap K L) P
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
⊢ ↑(aeval r) (↑derivative P) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
hmo : Monic P
hP : Splits (algebraMap K L) P
r : L
hr : r ∈ roots (map (algebraMap K L) P)
⊢ ↑(aeval r) (↑derivative P) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
replace hmo := hmo.map (algebraMap K L)
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ ↑(aeval r) (↑derivative P) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
hP : Splits (algebraMap K L) P
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
⊢ ↑(aeval r) (↑derivative P) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
replace hP := (splits_id_iff_splits (algebraMap K L)).2 hP
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ eval r (↑derivative (map (algebraMap K L) P)) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ ↑(aeval r) (↑derivative P) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
rw [aeval_def, ← eval_map, ← derivative_map]
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map (algebraMap K L) P))))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ eval r (↑derivative (map (algebraMap K L) P)) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
nth_rw 1 [eq_prod_roots_of_monic_of_splits_id hmo hP]
no goals
F : Type u
K : Type v
L : Type w
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Field F
i : K →+* L
inst✝ : Algebra K L
P : K[X]
r : L
hr : r ∈ roots (map (algebraMap K L) P)
hmo : Monic (map (algebraMap K L) P)
hP : Splits (RingHom.id L) (map (algebraMap K L) P)
⊢ eval r (↑derivative (Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map (algebraMap K L) P))))) =
    Multiset.prod (Multiset.map (fun a => r - a) (Multiset.erase (roots (map (algebraMap K L) P)) r))
rw [eval_multiset_prod_X_sub_C_derivative hr]