smeval_X_mul — Mathlib

English

For all n ∈ ℕ, smeval of X^n · p equals x^n times smeval of p: (X^n · p).smeval x = x^n · p.smeval x.

Русский

Для всех n ∈ ℕ, smeval (X^n · p) = x^n · p.smeval x.

LaTeX

$$$$ (X^n \cdot p).smeval x = x^n \cdot p.smeval x. $$$$

Lean4

theorem smeval_X_mul : (X * p).smeval x = x * p.smeval x := by
  induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [smeval_add, ph, qh, mul_add]
  | monomial n a =>
    rw [← monomial_one_one_eq_X, monomial_mul_monomial, smeval_monomial, one_mul, npow_add, npow_one, ← mul_smul_comm,
      smeval_monomial]

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