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
⊢ (sum p fun e a => ↑(RingHom.id R) a * x ^ e) = sum p fun e a => a * x ^ e
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 p = sum p fun e a => a * x ^ e
rw [eval, eval₂_eq_sum]
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
⊢ (sum p fun e a => ↑(RingHom.id R) a * x ^ e) = sum p fun e a => a * x ^ e
rfl