smeval_mul_X_pow — Mathlib

English

For every natural number n, the smeval map commutes with multiplying by X^n: smeval_x(p X^n) = smeval_x(p) · x^n.

Русский

Для любого натурального числа n отображение smeval при x удовлетворяет: smeval_x(p X^n) = smeval_x(p) · x^n.

LaTeX

$$$\forall n \in \mathbb{N},\; (p \cdot X^{n}).smeval\ x = p.smeval\ x \cdot x^{n}$$$

Lean4

theorem smeval_mul_X_pow : ∀ (n : ℕ), (p * X ^ n).smeval x = p.smeval x * x ^ n
  | 0 => by simp only [npow_zero, mul_one]
  | n + 1 => by
    rw [npow_add, ← mul_assoc, npow_one, smeval_mul_X, smeval_mul_X_pow n, npow_add, ← smeval_assoc_X_pow, npow_one]

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