eval₂_eq_zero_of_dvd_of_eval₂_eq_zero

Mathlib.Algebra.Polynomial.Eval.Defs

URI: https://scilib.ai/kg/mathlib#Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero

English

If p divides q and eval₂ f x p = 0, then eval₂ f x q = 0.

Русский

Если p делит q и eval₂ f x p = 0, то eval₂ f x q = 0.

LaTeX

$$$\text{if } p \mid q\text{ and } \operatorname{ev}_{f,x}(p) = 0\text{ then } \operatorname{ev}_{f,x}(q) = 0$$$

Lean4

theorem eval₂_eq_zero_of_dvd_of_eval₂_eq_zero (h : p ∣ q) (h0 : eval₂ f x p = 0) : eval₂ f x q = 0 :=
  zero_dvd_iff.mp (h0 ▸ eval₂_dvd f x h)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru