eval_smul — Mathlib

English

For a semiring R and S with an S-action on R, and s in S, (s • p).eval x = s • p.eval x.

Русский

Пусть S действует на R и p — полином над R. Тогда (s • p).eval x = s • p.eval x.

LaTeX

$$$ (s \\cdot p).eval x = s \\cdot p.eval x $$$

Lean4

@[simp]
theorem eval_smul [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : R[X]) (x : R) :
    (s • p).eval x = s • p.eval x := by
  rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul, eval₂_id]

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