R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Field R
p q : R[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : Finset.prod s f ≠ 0
⊢ ↑(Multiset.toFinset (roots (map (algebraMap R S) (Finset.prod s f)))) =
    ⋃ (i : ι) (_ : i ∈ ↑s), ↑(Multiset.toFinset (roots (map (algebraMap R S) (f i))))
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Field R
p q : R[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : Finset.prod s f ≠ 0
⊢ rootSet (Finset.prod s f) S = ⋃ (i : ι) (_ : i ∈ s), rootSet (f i) S
simp only [rootSet, ← Finset.mem_coe]
case a
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Field R
p q : R[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : Finset.prod s f ≠ 0
⊢ ∏ i in s, map (algebraMap R S) (f i) ≠ 0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Field R
p q : R[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : Finset.prod s f ≠ 0
⊢ ↑(Multiset.toFinset (roots (map (algebraMap R S) (Finset.prod s f)))) =
    ⋃ (i : ι) (_ : i ∈ ↑s), ↑(Multiset.toFinset (roots (map (algebraMap R S) (f i))))
rw [Polynomial.map_prod, roots_prod, Finset.bind_toFinset, s.val_toFinset, Finset.coe_biUnion]
no goals
case a
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝³ : Field R
p q : R[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra R S
ι : Type u_1
f : ι → R[X]
s : Finset ι
h : Finset.prod s f ≠ 0
⊢ ∏ i in s, map (algebraMap R S) (f i) ≠ 0
rwa [← Polynomial.map_prod, Ne, map_eq_zero]