R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
L : List R[X]
hd : R[X]
tl : List R[X]
ih : ¬0 ∈ tl → roots (List.prod tl) = Multiset.bind (↑tl) roots
H : ¬0 = hd ∧ ¬0 ∈ tl
⊢ roots (List.prod (hd :: tl)) = Multiset.bind (↑(hd :: tl)) roots
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
L : List R[X]
hd : R[X]
tl : List R[X]
ih : ¬0 ∈ tl → roots (List.prod tl) = Multiset.bind (↑tl) roots
H : ¬0 ∈ hd :: tl
⊢ roots (List.prod (hd :: tl)) = Multiset.bind (↑(hd :: tl)) roots
rw [List.mem_cons, not_or] at H
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]
L : List R[X]
hd : R[X]
tl : List R[X]
ih : ¬0 ∈ tl → roots (List.prod tl) = Multiset.bind (↑tl) roots
H : ¬0 = hd ∧ ¬0 ∈ tl
⊢ roots (List.prod (hd :: tl)) = Multiset.bind (↑(hd :: tl)) roots
rw [List.prod_cons, roots_mul (mul_ne_zero (Ne.symm H.1) <| List.prod_ne_zero H.2), ←
  Multiset.cons_coe, Multiset.cons_bind, ih H.2]