case ofFinsupp
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
n : ℕ
a : R
p : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * ↑C a) n = coeff { toFinsupp := p } n * a
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
a : R
⊢ coeff (p * ↑C a) n = coeff p n * a
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]
n : ℕ
a : R
p : AddMonoidAlgebra R ℕ
⊢ ↑(p * Finsupp.single 0 a) n = ↑p n * a
case ofFinsupp
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
n : ℕ
a : R
p : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * ↑C a) n = coeff { toFinsupp := p } n * a
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]
n : ℕ
a : R
p : AddMonoidAlgebra R ℕ
⊢ ↑(p * Finsupp.single 0 a) n = ↑p n * a
exact AddMonoidAlgebra.mul_single_zero_apply p a n