Theorem: SkewPolynomial.toFinsupp_eq_zero (SkewPolynomials.lean)

State before:
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q a : R[X;φ]
⊢ a.toFinsupp = 0 ↔ a = 0
Tactic:
rw [← toFinsupp_zero, toFinsupp_inj]
State after:
no goals