Theorem: SkewPolynomial.toFinsupp_sub (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 b : S[X;φ]
⊢ (a - b).toFinsupp = a.toFinsupp - b.toFinsupp
Tactic:
rw [sub_eq_add_neg, ← toFinsupp_neg, ← toFinsupp_add]
State after:
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 b : S[X;φ]
⊢ (a - b).toFinsupp = (a + -b).toFinsupp

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 b : S[X;φ]
⊢ (a - b).toFinsupp = (a + -b).toFinsupp
Tactic:
rfl
State after:
no goals