∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A)
  (p : Polynomial R),
  (polyEquivTensor R A).symm (a ⊗ₜ[R] p) = p.sum fun n r => (Polynomial.monomial n) (a * (algebraMap R A) r)