R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ (sum p fun e a => ↑(monomial e) a) = p
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp p X = p
simp only [comp, eval₂_def, C_mul_X_pow_eq_monomial]
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]
⊢ (sum p fun e a => ↑(monomial e) a) = p
exact sum_monomial_eq _