aeval_eq_zero_of_dvd_aeval_eq_zero

English

Let S be a commutative semiring and T a commutative semiring with an S-algebra structure. If p divides q in S[X] and a ∈ T satisfies aeval a p = 0, then aeval a q = 0.

Русский

Пусть S, T — коммутативные полугруппы без нуля, обладающие структурой S-алгебры. Если p делит q в S[X] и a ∈ T удовлетворяет aeval a p = 0, то aeval a q = 0.

LaTeX

$$$(\exists p,q \in S[X])(p \mid q) \land aeval\,a\,p = 0 \Rightarrow aeval\,a\,q = 0$$$

Lean4

theorem aeval_eq_zero_of_dvd_aeval_eq_zero [CommSemiring S] [CommSemiring T] [Algebra S T] {p q : S[X]} (h₁ : p ∣ q)
    {a : T} (h₂ : aeval a p = 0) : aeval a q = 0 :=
  by
  rw [aeval_def, ← eval_map] at h₂ ⊢
  exact eval_eq_zero_of_dvd_of_eval_eq_zero (Polynomial.map_dvd (algebraMap S T) h₁) h₂

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