R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
⊢ (sum p fun e a => ↑C (↑(algebraMap R S) a) * X ^ e) = sum p fun e a => (↑C ∘ ↑(algebraMap R S)) a * X ^ e
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
⊢ ↑(mapAlg R S) p = map (algebraMap R S) p
simp only [mapAlg, aeval_def, eval₂_eq_sum, map, algebraMap_apply, RingHom.coe_comp]
case a
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n✝ : ℕ
⊢ coeff (sum p fun e a => ↑C (↑(algebraMap R S) a) * X ^ e) n✝ =
    coeff (sum p fun e a => (↑C ∘ ↑(algebraMap R S)) a * X ^ e) n✝
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
⊢ (sum p fun e a => ↑C (↑(algebraMap R S) a) * X ^ e) = sum p fun e a => (↑C ∘ ↑(algebraMap R S)) a * X ^ e
ext
no goals
case a
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : Semiring S
inst✝ : Algebra R S
p : R[X]
n✝ : ℕ
⊢ coeff (sum p fun e a => ↑C (↑(algebraMap R S) a) * X ^ e) n✝ =
    coeff (sum p fun e a => (↑C ∘ ↑(algebraMap R S)) a * X ^ e) n✝
congr