X_sub_C_dvd_sub_C_eval

Mathlib.Algebra.Polynomial.Div

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem X_sub_C_dvd_sub_C_eval : X - C a ∣ p - C (p.eval a) := by
  rw [dvd_iff_isRoot, IsRoot, eval_sub, eval_C, sub_self]
    -- TODO: generalize this to Ring. In general, 0 can be replaced by any element in the center of R.

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

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

Разделы

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

Аффилиация

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