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