smeval_X_pow_assoc — Mathlib

English

For the monomial n with coefficient r, smeval of (monomial n r · p) equals r times smeval of (x^n · p): (monomial n r · p).smeval x = r • (x^n · p.smeval x).

Русский

Для монома n c(const) r, smeval (monomial n r · p) = r · (x^n · p.smeval x).

LaTeX

$$$$ (\\mathrm{monomial}\\ n\ \ r\\cdot p).smeval x = r \\cdot (x^n \\cdot p.smeval x). $$$$

Lean4

theorem smeval_X_pow_assoc (m n : ℕ) : x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * 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 => simp only [smeval_monomial, mul_smul_comm, npow_mul_assoc]

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