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
p q : R[X]
hp : eval₂ C X p = p
hq : eval₂ C X q = q
⊢ eval₂ C X (p + q) = p + q
simp [hp, hq]
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
n : ℕ
x : R
⊢ eval₂ C X (↑(monomial n) x) = ↑(monomial n) x
rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']