case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (r • { toFinsupp := toFinsupp✝ }) n = r • coeff { toFinsupp := toFinsupp✝ } n
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
p : R[X]
n : ℕ
⊢ coeff (r • p) n = r • coeff p n
rcases p with ⟨⟩
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(r • toFinsupp✝) n = r • ↑toFinsupp✝ n
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (r • { toFinsupp := toFinsupp✝ }) n = r • coeff { toFinsupp := toFinsupp✝ } n
simp_rw [← ofFinsupp_smul, coeff]
no goals
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(r • toFinsupp✝) n = r • ↑toFinsupp✝ n
exact Finsupp.smul_apply _ _ _