no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ eval x (↑C a * p) = a * eval x p
induction p using Polynomial.induction_on' with
| h_add p q ph qh =>
  simp only [mul_add, eval_add, ph, qh]
| h_monomial n b =>
  simp only [mul_assoc, C_mul_monomial, eval_monomial]
no goals
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
x : R
p q : R[X]
ph : eval x (↑C a * p) = a * eval x p
qh : eval x (↑C a * q) = a * eval x q
⊢ eval x (↑C a * (p + q)) = a * eval x (p + q)
simp only [mul_add, eval_add, ph, qh]
no goals
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
n : ℕ
b : R
⊢ eval x (↑C a * ↑(monomial n) b) = a * eval x (↑(monomial n) b)
simp only [mul_assoc, C_mul_monomial, eval_monomial]