eval_mul_X — Mathlib

English

Multiplication by the indeterminate X shifts degree and corresponds to multiplying the evaluation by x: (p * X).eval x = p.eval x · x.

Русский

Умножение на индетерминант X сдвигает степень и соответствует умножению значения оценивания на x: (p · X).eval x = p.eval x · x.

LaTeX

$$$ (p \cdot X).\mathrm{eval}\ x = p.\mathrm{eval}\ x \cdot x $$$

Lean4

@[simp]
theorem eval_mul_X : (p * X).eval x = p.eval x * x :=
  eval₂_mul_X ..

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