R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
⊢ (Finset.sum (support p) fun x => a • (↑(algebraMap R A[X]) (coeff p x) * X ^ x)) =
    Finset.sum (support p) fun x => ↑(monomial x) (a * ↑(algebraMap R A) (coeff p x))
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
⊢ ↑(↑(toFunBilinear R A) a) p = sum p fun n r => ↑(monomial n) (a * ↑(algebraMap R A) r)
simp only [toFunBilinear_apply_apply, aeval_def, eval₂_eq_sum, Polynomial.sum, Finset.smul_sum]
case e_f.h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
i : ℕ
⊢ a • (↑(algebraMap R A[X]) (coeff p i) * X ^ i) = ↑(monomial i) (a * ↑(algebraMap R A) (coeff p i))
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
⊢ (Finset.sum (support p) fun x => a • (↑(algebraMap R A[X]) (coeff p x) * X ^ x)) =
    Finset.sum (support p) fun x => ↑(monomial x) (a * ↑(algebraMap R A) (coeff p x))
congr with i : 1
no goals
case e_f.h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
i : ℕ
⊢ a • (↑(algebraMap R A[X]) (coeff p i) * X ^ i) = ↑(monomial i) (a * ↑(algebraMap R A) (coeff p i))
rw [← Algebra.smul_def, ← C_mul', mul_smul_comm, C_mul_X_pow_eq_monomial, ← Algebra.commutes,
  ← Algebra.smul_def, smul_monomial]