case a
R : Type u
S : Type v
a✝ b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
f : R[X]
n✝ : ℕ
⊢ coeff (↑C a * f) n✝ = coeff (a • f) n✝
R : Type u
S : Type v
a✝ b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
f : R[X]
⊢ ↑C a * f = a • f
ext
no goals
case a
R : Type u
S : Type v
a✝ b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
f : R[X]
n✝ : ℕ
⊢ coeff (↑C a * f) n✝ = coeff (a • f) n✝
rw [coeff_C_mul, coeff_smul, smul_eq_mul]