English
The smeval of p · X equals smeval(p) times x: (p · X).smeval x = p.smeval x · x.
Русский
Smeval(p · X) = Smeval(p) · X: (p · X).smeval x = p.smeval x · x.
LaTeX
$$$$ (p \cdot X).smeval x = p.smeval x \cdot x. $$$$
Lean4
theorem smeval_mul_X : (p * X).smeval x = p.smeval x * x := by
induction p using Polynomial.induction_on' with
| add p q ph qh => simp only [add_mul, smeval_add, ph, qh]
| monomial n a =>
simp only [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, mul_one, npow_add, smul_mul_assoc,
npow_one]