smeval_monomial_mul — Mathlib

English

For p ∈ R[X] and n ∈ ℕ, smeval of (X^n · p) equals x^n times smeval of p: (X^n · p).smeval x = x^n · p.smeval x.

Русский

Для p ∈ R[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_monomial_mul (n : ℕ) : (monomial n r * p).smeval x = r • (x ^ n * p.smeval x) := by
  induction p using Polynomial.induction_on' with
  | add r s hr hs =>
    simp only [smeval_add]
    rw [← C_mul_X_pow_eq_monomial, mul_assoc, smeval_C_mul, smeval_X_pow_mul, smeval_add]
  | monomial n a => rw [smeval_monomial, monomial_mul_monomial, smeval_monomial, npow_add, mul_smul, mul_smul_comm]

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