no goals
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬coeff p k = 0
a : A
⊢ (if ¬coeff p k = 0 then a * ↑(algebraMap R A) (coeff p k) else 0) = a * ↑(algebraMap R A) (coeff p k)
classical split_ifs <;> simp [*]
no goals
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬coeff p k = 0
a : A
⊢ (if ¬coeff p k = 0 then a * ↑(algebraMap R A) (coeff p k) else 0) = a * ↑(algebraMap R A) (coeff p k)
split_ifs <;> simp [*]