case ofFinsupp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
p : AddMonoidAlgebra R ℕ
⊢ coeff (↑C a * { toFinsupp := p }) n = a * coeff { toFinsupp := p } n
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ coeff (↑C a * p) n = a * coeff p n
rcases p with ⟨p⟩
case ofFinsupp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
p : AddMonoidAlgebra R ℕ
⊢ ↑(Finsupp.single 0 a * p) n = a * ↑p n
case ofFinsupp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
p : AddMonoidAlgebra R ℕ
⊢ coeff (↑C a * { toFinsupp := p }) n = a * coeff { toFinsupp := p } n
simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
no goals
case ofFinsupp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
p : AddMonoidAlgebra R ℕ
⊢ ↑(Finsupp.single 0 a * p) n = a * ↑p n
exact AddMonoidAlgebra.single_zero_mul_apply p a n