case h.e'_2
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p)) =
    ↑C (leadingCoeff p) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p)) = p
convert C_leadingCoeff_mul_prod_multiset_X_sub_C hroots
no goals
case h.e'_2
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp : Monic p
hroots : ↑Multiset.card (roots p) = natDegree p
⊢ Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p)) =
    ↑C (leadingCoeff p) * Multiset.prod (Multiset.map (fun a => X - ↑C a) (roots p))
rw [hp.leadingCoeff, C_1, one_mul]