no goals
R : Type u
S : Type v
T : Type w
A : Type z
A' : Type ?u.1112049
B' : Type ?u.1112052
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.1112265
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
p : R[X]
⊢ coeff p 0 = ↑(aeval 0) p
simp [coeff_zero_eq_eval_zero]