smeval_mul_X — Mathlib

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]

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