R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (List.prod (List.map (↑(aeval a)) (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p)))))
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (↑(aeval a) (Multiset.prod (Multiset.map (fun x => X - ↑C x) (roots p))))
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
rw [← Multiset.prod_toList, AlgHom.map_list_prod] at h
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h :
  ¬∀ (m : (fun x => A) (List.prod (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p))))),
      m ∈ List.map (↑(aeval a)) (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p))) → IsUnit m
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ¬IsUnit (List.prod (List.map (↑(aeval a)) (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p)))))
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
replace h := mt List.prod_isUnit h
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ∃ a_1, a_1 ∈ roots p ∧ ¬IsUnit (a - ↑↑ₐ a_1)
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h :
  ¬∀ (m : (fun x => A) (List.prod (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p))))),
      m ∈ List.map (↑(aeval a)) (Multiset.toList (Multiset.map (fun x => X - ↑C x) (roots p))) → IsUnit m
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X,
  exists_exists_and_eq_and, Multiset.mem_map, AlgHom.map_sub] at h
case intro.intro
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ roots p
r_nu : ¬IsUnit (a - ↑↑ₐ r)
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
h : ∃ a_1, a_1 ∈ roots p ∧ ¬IsUnit (a - ↑↑ₐ a_1)
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
rcases h with ⟨r, r_mem, r_nu⟩
no goals
case intro.intro
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ roots p
r_nu : ¬IsUnit (a - ↑↑ₐ r)
⊢ ∃ k, k ∈ σ a ∧ eval k p = 0
exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], (mem_roots'.1 r_mem).2⟩
no goals
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : IsDomain R
p : R[X]
a : A
r : R
r_mem : r ∈ roots p
r_nu : ¬IsUnit (a - ↑↑ₐ r)
⊢ r ∈ σ a
rwa [mem_iff, ← IsUnit.sub_iff]