mv_polynomial composition

Stream: general

[AG]

Is there already some sort of way to show that the composition of multivariate polynomials is still a multivariate polynomial? In particular, I'd like:

 -- The composition of two polynomials is still a polynomial
  def comp: mv_polynomial σ α → (σ → mv_polynomial τ α) → mv_polynomial τ α :=
    sorry

  -- The evaluation of the composition is the same as the composition of the evaluations
  lemma formal_comp_eq_eval_comp (p: mv_polynomial σ α) (q: σ → mv_polynomial τ α) (f: τ → α):
    mv_polynomial.eval (λs:σ, mv_polynomial.eval f (q s)) p = mv_polynomial.eval f (comp p q) :=
  begin
    sorry
  end

[Anne Baanen]

The first is docs#mv_polynomial.bind₁.

[Anne Baanen]

Polynomials form a monad! :D

[Johan Commelin]

In two different ways! :D

[Johan Commelin]

Does docs#mv_polynomial.eval_bind₁ exist?

[Johan Commelin]

Doesn't look like it :sad: