R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Finset R
⊢ (Multiset.bind s.val fun i => roots (X - ↑C i)) = s.val

R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Finset R
⊢ (Finset.prod s fun a => X - ↑C a) ≠ 0
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Finset R
⊢ roots (Finset.prod s fun a => X - ↑C a) = s.val
apply (roots_prod (fun a => X - C a) s ?_).trans
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Finset R
⊢ (Multiset.bind s.val fun i => {i}) = s.val
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Finset R
⊢ (Multiset.bind s.val fun i => roots (X - ↑C i)) = s.val
simp_rw [roots_X_sub_C]
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Finset R
⊢ (Multiset.bind s.val fun i => {i}) = s.val
rw [Multiset.bind_singleton, Multiset.map_id']
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
s : Finset R
⊢ (Finset.prod s fun a => X - ↑C a) ≠ 0
refine prod_ne_zero_iff.mpr (fun a _ => X_sub_C_ne_zero a)