aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C

English

If the mapAlg of a polynomial p equals a product over a multiset s of factors X − a, and x is a root in the target ring, then evaluating p at x gives zero.

Русский

Если mapAlg p равен произведению по множеству s факторов X − a, и x является корнем в целевом кольце, тогда при подстановке x в p получается нуль.

LaTeX

$$$\text{mapAlg}_R^L(p) = \prod_{a\in s}(X - C(a)) \Rightarrow \operatorname{aeval}_x(p) = 0$$$

Lean4

theorem aeval_root_of_mapAlg_eq_multiset_prod_X_sub_C [CommSemiring R] [CommRing L] [Algebra R L] (s : Multiset L)
    {x : L} (hx : x ∈ s) {p : R[X]} (hp : mapAlg R L p = (Multiset.map (fun a : L ↦ X - C a) s).prod) : aeval x p = 0 :=
  by
  rw [← aeval_map_algebraMap L, ← mapAlg_eq_map, hp, map_multiset_prod, Multiset.prod_eq_zero]
  rw [Multiset.map_map, Multiset.mem_map]
  exact ⟨x, hx, by simp⟩

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