R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : SMulZeroClass S R
a : S
n : ℕ
b : R
⊢ a • Finsupp.single n b = Finsupp.single n (a • b)
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : SMulZeroClass S R
a : S
n : ℕ
b : R
⊢ (a • ↑(monomial n) b).toFinsupp = (↑(monomial n) (a • b)).toFinsupp
simp
no goals
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : SMulZeroClass S R
a : S
n : ℕ
b : R
⊢ a • Finsupp.single n b = Finsupp.single n (a • b)
rw [smul_single]