Theorem: SkewPolynomial.ofFinsupp_neg (SkewPolynomials.lean)

State before:
R : Type u
a✝ b : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a : AddMonoidAlgebra S ℕ
⊢ { toFinsupp := -a } = SkewPolynomial.neg { toFinsupp := a }
Tactic:
rw [neg_def]
State after:
no goals