eval_eq_zero_of_dvd_of_eval_eq_zero

English

If p divides q, then evaluating at x preserves divisibility: eval x p divides eval x q.

Русский

Если p делит q, то при оценивании в x выполняется делимость: eval x p делит eval x q.

LaTeX

$$$\\text{p} \\mid \\text{q} \\Rightarrow \\text{eval}_x(\\text{p}) \\mid \\text{eval}_x(\\text{q})$$$

Lean4

theorem eval_eq_zero_of_dvd_of_eval_eq_zero : p ∣ q → eval x p = 0 → eval x q = 0 :=
  eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _

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