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₂