eval_C_mul — Mathlib

English

Multiplication by a constant commutes with evaluation: (C a * p).eval x = a * p.eval x.

Русский

Умножение на константу коммутирует с оцениванием: (C a · p).eval x = a · p.eval x.

LaTeX

$$$ (C\ a \cdot p).\mathrm{eval}\ x = a \cdot p.\mathrm{eval}\ x $$$

Lean4

@[simp]
theorem eval_C_mul : (C a * p).eval x = a * p.eval x := by
  induction p using Polynomial.induction_on' with
  | add p q ph qh => simp only [mul_add, eval_add, ph, qh]
  | monomial n b => simp only [mul_assoc, C_mul_monomial, eval_monomial]

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