∀ (R : Type u_2) (S : Type u_3) (T : Type u_1) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra S T] (x : Polynomial R) (x_1 : S → T) (z : S),
  (x • x_1) z =
    ({ toFun := fun p z => (algebraMap S T) ((Polynomial.aeval z) p), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
            map_add' := ⋯ }
          x *
        x_1)
      z