Theorem: SkewPolynomial.ofFinsupp_mul (SkewPolynomials.lean)

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