theorem Hex.DensePoly.eval_scale_semiring {S : Type u} [Lean.Grind.CommSemiring S] [DecidableEq S] (c : S) (p : DensePoly S) (x : S) : (scale c p).eval x = c * p.eval x

Horner evaluation commutes with coefficientwise scaling.

theorem Hex.DensePoly.eval_shift_semiring {S : Type u} [Lean.Grind.CommSemiring S] [DecidableEq S] (n : Nat) (p : DensePoly S) (x : S) : (shift n p).eval x = p.eval x * x ^ n

Horner evaluation turns a degree shift into multiplication by x ^ n.

@[simp]

theorem Hex.DensePoly.eval_mul_commring {S : Type u} [Lean.Grind.CommRing S] [DecidableEq S] (p q : DensePoly S) (x : S) : (p * q).eval x = p.eval x * q.eval x

Horner evaluation is multiplicative.