eval₂_mul_eq_zero_of_right — Mathlib

English

Another restatement of zero transfer for right factor under evaluation.

Русский

Ещё одно переформулирование переноса нуля для правого множителя при оценке.

LaTeX

$$$\text{If } \operatorname{ev}_{f,x}(q) = 0 \text{ then } (p q).\operatorname{ev}_{f,x} = 0$$$

Lean4

theorem eval₂_mul_eq_zero_of_right (p : R[X]) (hq : q.eval₂ f x = 0) : (p * q).eval₂ f x = 0 :=
  by
  rw [eval₂_mul f x]
  exact mul_eq_zero_of_right (p.eval₂ f x) hq

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