case mk
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
ι : Type u_1
f : ι → R[X]
m : Multiset ι
hm : Nodup m
⊢ Finset.prod { val := m, nodup := hm } f ≠ 0 →
    roots (Finset.prod { val := m, nodup := hm } f) = Multiset.bind { val := m, nodup := hm }.val fun i => roots (f i)
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
ι : Type u_1
f : ι → R[X]
s : Finset ι
⊢ Finset.prod s f ≠ 0 → roots (Finset.prod s f) = Multiset.bind s.val fun i => roots (f i)
rcases s with ⟨m, hm⟩
no goals
case mk
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
ι : Type u_1
f : ι → R[X]
m : Multiset ι
hm : Nodup m
⊢ Finset.prod { val := m, nodup := hm } f ≠ 0 →
    roots (Finset.prod { val := m, nodup := hm } f) = Multiset.bind { val := m, nodup := hm }.val fun i => roots (f i)
simpa [Multiset.prod_eq_zero_iff, Multiset.bind_map] using roots_multiset_prod (m.map f)