case mp
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
⊢ Splits (RingHom.id K) p → ↑Multiset.card (roots p) = natDegree p

case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
⊢ ↑Multiset.card (roots p) = natDegree p → Splits (RingHom.id K) 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]
⊢ Splits (RingHom.id K) p ↔ ↑Multiset.card (roots p) = natDegree p
constructor
case mp
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
H : Splits (RingHom.id K) p
⊢ ↑Multiset.card (roots p) = natDegree p
case mp
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
⊢ Splits (RingHom.id K) p → ↑Multiset.card (roots p) = natDegree p
intro H
no goals
case mp
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
H : Splits (RingHom.id K) p
⊢ ↑Multiset.card (roots p) = natDegree p
rw [natDegree_eq_card_roots H, map_id]
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ Splits (RingHom.id K) p
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
⊢ ↑Multiset.card (roots p) = natDegree p → Splits (RingHom.id K) p
intro hroots
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ ∃ s, map (RingHom.id K) p = ↑C (↑(RingHom.id K) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ Splits (RingHom.id K) p
rw [splits_iff_exists_multiset (RingHom.id K)]
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ map (RingHom.id K) p =
    ↑C (↑(RingHom.id K) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ ∃ s, map (RingHom.id K) p = ↑C (↑(RingHom.id K) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) s)
use p.roots
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ p = ↑C (leadingCoeff p) * Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots p))
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ map (RingHom.id K) p =
    ↑C (↑(RingHom.id K) (leadingCoeff p)) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))
simp only [RingHom.id_apply, map_id]
no goals
case mpr
F : Type u
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Field F
i : K →+* L
p : K[X]
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ p = ↑C (leadingCoeff p) * Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots p))
exact (C_leadingCoeff_mul_prod_multiset_X_sub_C hroots).symm