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]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p = eval x (map f p)
induction p using Polynomial.induction_on' with
| h_add p q hp hq =>
  simp [hp, hq]
| h_monomial n r =>
  simp
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]
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[X]
hp : eval₂ f x p = eval x (map f p)
hq : eval₂ f x q = eval x (map f q)
⊢ eval₂ f x (p + q) = eval x (map f (p + q))
simp [hp, hq]
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]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
r : R
⊢ eval₂ f x (↑(monomial n) r) = eval x (map f (↑(monomial n) r))
simp