eval₂_mul_C' — Mathlib

English

Multiplying a polynomial by X corresponds to multiplying its evaluation by x.

Русский

Умножение полинома на X соответствует умножению его оценки на x.

LaTeX

$$$\operatorname{ev}_{f,x}(p \cdot X) = \operatorname{ev}_{f,x}(p) \cdot x$$$

Lean4

theorem eval₂_mul_C' (h : Commute (f a) x) : eval₂ f x (p * C a) = eval₂ f x p * f a :=
  by
  rw [eval₂_mul_noncomm, eval₂_C]
  intro k
  by_cases hk : k = 0
  · simp only [hk, h, coeff_C_zero]
  · simp only [coeff_C_ne_zero hk, RingHom.map_zero, Commute.zero_left]

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