mod_X_sub_C_eq_C_eval — Mathlib

English

For any p and a in R, the remainder of p modulo X − C a equals the constant polynomial C(p(a)).

Русский

Для любого p и a из R остаток от деления p на X − C a равен константному многочлену C(p(a)).

LaTeX

$$$ p \bmod (X - C a) = C\bigl(p(a)\bigr) $$$

Lean4

theorem mod_X_sub_C_eq_C_eval (p : R[X]) (a : R) : p % (X - C a) = C (p.eval a) :=
  modByMonic_eq_mod p (monic_X_sub_C a) ▸ modByMonic_X_sub_C_eq_C_eval _ _

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