Zulip Chat Archive

Stream: general

Topic: mv_polynomial composition

AG (Jun 15 2021 at 14:00):

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 τ α :=

  -- 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) :=

Anne Baanen (Jun 15 2021 at 14:04):

The first is docs#mv_polynomial.bind₁.

Anne Baanen (Jun 15 2021 at 14:06):

Polynomials form a monad! :D

Johan Commelin (Jun 15 2021 at 14:11):

In two different ways! :D

Johan Commelin (Jun 15 2021 at 14:12):

Does docs#mv_polynomial.eval_bind₁ exist?

Johan Commelin (Jun 15 2021 at 14:13):

Doesn't look like it :sad:

Last updated: Aug 03 2023 at 10:10 UTC