smeval_X_pow_mul — Mathlib

English

The smeval of monomial times p distributes as in the previous rule: smeval of monomial n r times p equals r times smeval of p times x^n.

Русский

С smeval монома умножение соблюдает распределение: 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_mul : ∀ (n : ℕ), (X ^ n * p).smeval x = x ^ n * p.smeval x
  | 0 => by simp [npow_zero, one_mul]
  | n + 1 => by
    rw [add_comm, npow_add, mul_assoc, npow_one, smeval_X_mul, smeval_X_pow_mul n, npow_add, smeval_X_pow_assoc,
      npow_one]

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