F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ map i p = ↑C (leadingCoeff (map i p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i 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]
i : K →+* L
hsplit : Splits i p
⊢ map i p = ↑C (↑i (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p)))
rw [← leadingCoeff_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]
i : K →+* L
hsplit : Splits i p
⊢ ↑C (leadingCoeff (map i p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) = map i 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]
i : K →+* L
hsplit : Splits i p
⊢ map i p = ↑C (leadingCoeff (map i p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p)))
symm
case hroots
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ ↑Multiset.card (roots (map i p)) = natDegree (map i 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]
i : K →+* L
hsplit : Splits i p
⊢ ↑C (leadingCoeff (map i p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots (map i p))) = map i p
apply C_leadingCoeff_mul_prod_multiset_X_sub_C
case hroots
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ ↑Multiset.card (roots (map i p)) = natDegree p
case hroots
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ ↑Multiset.card (roots (map i p)) = natDegree (map i p)
rw [natDegree_map]
no goals
case hroots
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i✝ : K →+* L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ ↑Multiset.card (roots (map i p)) = natDegree p
exact (natDegree_eq_card_roots hsplit).symm