sub_dvd_eval_sub

Mathlib.Algebra.Polynomial.Div

URI: https://scilib.ai/kg/mathlib#Polynomial.sub_dvd_eval_sub

← MathLib Explorer

English

For a,b ∈ R and p ∈ R[X], a − b divides p(a) − p(b).

Русский

Для a,b ∈ R и p ∈ R[X], a − b делит p(a) − p(b).

LaTeX

$$$ a - b \mid p(a) - p(b) $$$

Lean4

theorem sub_dvd_eval_sub (a b : R) (p : R[X]) : a - b ∣ p.eval a - p.eval b :=
  by
  suffices X - C b ∣ p - C (p.eval b) by
    simpa only [coe_evalRingHom, eval_sub, eval_X, eval_C] using (_root_.map_dvd (evalRingHom a)) this
  simp [dvd_iff_isRoot]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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