R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff { toFinsupp := Finsupp.single n a } m = if n = m then a else 0
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (↑(monomial n) a) m = if n = m then a else 0
rw [← ofFinsupp_single]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑(Finsupp.single n a) m = if n = m then a else 0
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff { toFinsupp := Finsupp.single n a } m = if n = m then a else 0
simp only [coeff, LinearMap.coe_mk]
no goals
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑(Finsupp.single n a) m = if n = m then a else 0
rw [Finsupp.single_apply]