∀ {R : Type u} {N : Type v} [inst : CommSemiring R] {σ : Type u_1} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : DecidableEq σ] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  (p : MvPolynomial σ S) (n : N) (d : σ →₀ ℕ), (MvPolynomial.rTensor (p ⊗ₜ[R] n)) d = MvPolynomial.coeff d p ⊗ₜ[R] n