case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q b : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } * b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp * b.toFinsupp
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
p q a b : R[X]
⊢ (a * b).toFinsupp = a.toFinsupp * b.toFinsupp
cases a
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp * { toFinsupp := toFinsupp✝ }.toFinsupp
case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q b : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } * b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp * b.toFinsupp
cases b
no goals
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp * { toFinsupp := toFinsupp✝ }.toFinsupp
rw [← ofFinsupp_mul]