∀ (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 : CommSemiring N] [inst_4 : Algebra R N] (f : σ → S) (p : MvPolynomial σ R),
  (MvPolynomial.aeval fun x => 1 ⊗ₜ[R] f x) p = 1 ⊗ₜ[R] (MvPolynomial.aeval f) p