case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ X * { toFinsupp := toFinsupp✝ } = { toFinsupp := toFinsupp✝ } * X
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ X * p = p * X
rcases p with ⟨⟩
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ Finsupp.single 1 1 * toFinsupp✝ = toFinsupp✝ * Finsupp.single 1 1
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ X * { toFinsupp := toFinsupp✝ } = { toFinsupp := toFinsupp✝ } * X
simp only [X, ← ofFinsupp_single, ← ofFinsupp_mul, LinearMap.coe_mk, ofFinsupp.injEq]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
x✝ : ℕ
⊢ ↑(Finsupp.single 1 1 * toFinsupp✝) x✝ = ↑(toFinsupp✝ * Finsupp.single 1 1) x✝
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ Finsupp.single 1 1 * toFinsupp✝ = toFinsupp✝ * Finsupp.single 1 1
refine Finsupp.ext fun _ => ?_
no goals
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
x✝ : ℕ
⊢ ↑(Finsupp.single 1 1 * toFinsupp✝) x✝ = ↑(toFinsupp✝ * Finsupp.single 1 1) x✝
simp [AddMonoidAlgebra.mul_apply, AddMonoidAlgebra.sum_single_index, add_comm]