case a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : roots (map i h) = {↑i x}
⊢ map i h = map i (↑C (leadingCoeff h) * (X - ↑C x))
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : roots (map i h) = {↑i x}
⊢ h = ↑C (leadingCoeff h) * (X - ↑C x)
apply Polynomial.map_injective _ i.injective
case a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : roots (map i h) = {↑i x}
⊢ ↑C (↑i (leadingCoeff h)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) {↑i x}) =
    map i (↑C (leadingCoeff h) * (X - ↑C x))
case a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : roots (map i h) = {↑i x}
⊢ map i h = map i (↑C (leadingCoeff h) * (X - ↑C x))
rw [eq_prod_roots_of_splits h_splits, h_roots]
no goals
case a
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
x : K
h : K[X]
h_splits : Splits i h
h_roots : roots (map i h) = {↑i x}
⊢ ↑C (↑i (leadingCoeff h)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) {↑i x}) =
    map i (↑C (leadingCoeff h) * (X - ↑C x))
simp