Theorem: SkewPolynomial.ofFinsupp_eq_one (SkewPolynomials.lean)

State before:
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a } = 1 ↔ a = 1
Tactic:
rw [← ofFinsupp_one, ofFinsupp_inj]
State after:
no goals