Topic: mv_polynomial composition
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 (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