smeval_add — Mathlib

English

Similarly, smeval of X^n is x^n for all n: (X^n).smeval x = x^n.

Русский

Аналогично, smeval X^n = x^n для любого n: (X^n).smeval x = x^n.

LaTeX

$$$$ (X^n : R[X]).smeval x = x^n. $$$$

Lean4

@[simp]
theorem smeval_add : (p + q).smeval x = p.smeval x + q.smeval x :=
  by
  simp only [smeval_eq_sum]
  refine sum_add_index p q (smul_pow x) (fun _ ↦ ?_) (fun _ _ _ ↦ ?_)
  · rw [smul_pow, zero_smul]
  · rw [smul_pow, smul_pow, smul_pow, add_smul]

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