∀ {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B]
  {x : σ → A} {p : MvPolynomial σ R},
  Function.Injective ⇑(algebraMap A B) →
    ((MvPolynomial.aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (MvPolynomial.aeval x) p = 0)