smeval_smul — Mathlib

English

Smeval is linear in the polynomial: smeval(r p) x = r · smeval(p) x.

Русский

Smeval линейна по полиному: smeval(r p) x = r · smeval(p) x.

LaTeX

$$$$ \forall p\in R[X], \forall r\in R, \forall x, (r \cdot p).smeval x = r \cdot p.smeval x. $$$$

Lean4

@[simp]
theorem smeval_smul (r : R) : (r • p).smeval x = r • p.smeval x := by
  induction p using Polynomial.induction_on' with
  | add p q ph qh => rw [smul_add, smeval_add, ph, qh, ← smul_add, smeval_add]
  | monomial n a => rw [smul_monomial, smeval_monomial, smeval_monomial, smul_assoc]

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