Evaluation of polynomials is associative

eval_assoc.lean

import linear_algebra.multivariate_polynomial

universes u v w

variables {σ : Type v} [decidable_eq σ]
variables {R : Type u} [decidable_eq R] [comm_ring R]
variables {τ : Type w} [decidable_eq τ]

open mv_polynomial

theorem eval_assoc₁
(f : mv_polynomial σ R) (g : σ → mv_polynomial τ R) (h : τ → R)
: f.eval (λ n : σ, (g n).eval h) = ((functorial C f).eval g).eval h :=
begin
  sorry
end

theorem eval_assoc₂
(f : mv_polynomial σ (mv_polynomial τ R)) (g : σ → mv_polynomial τ R) (h : τ → R)
: C ((f.eval g).eval h) = f.eval (λ n : σ, C ((g n).eval h)) :=
begin
  sorry
end