no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1127963
B' : Type ?u.1127966
a b : R
n : ℕ
inst✝⁶ : CommSemiring A'
inst✝⁵ : Semiring B'
inst✝⁴ : CommSemiring R
p✝ q : R[X]
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type ?u.1128179
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
⊢ ↑(algebraMap R A) (coeff p 0) = ↑(aeval 0) p
simp [aeval_def]