exists_mem_of_not_isUnit_aeval_prod

English

If a ∈ A yields a non-unit aeval in a product of roots, there exists k ∈ spectrum such that eval k p = 0.

Русский

Если x не является единицей в аeval произведения корней, существует k из спектра, для которого p(k)=0.

LaTeX

$$exists_mem_of_not_isUnit_aeval_prod$$

Lean4

theorem exists_mem_of_not_isUnit_aeval_prod [IsDomain R] {p : R[X]} {a : A}
    (h : ¬IsUnit (aeval a (Multiset.map (fun x : R => X - C x) p.roots).prod)) : ∃ k : R, k ∈ σ a ∧ eval k p = 0 :=
  by
  rw [← Multiset.prod_toList, map_list_prod] at h
  replace h := mt List.prod_isUnit h
  simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X, exists_exists_and_eq_and,
    Multiset.mem_map, map_sub] at h
  rcases h with ⟨r, r_mem, r_nu⟩
  exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], (mem_roots'.1 r_mem).2⟩

Похожие утверждения