Re: [isabelle] HOL/Library/Polynomial pcompose

Hi Walther,

Am 23.11.2013 15:24, schrieb Walther Neuper:
> the definition
>   definition pcompose :: "'a::comm_semiring_0 poly => 'a poly => 'a poly"
>   where
>     "pcompose p q = fold_coeffs (λa c. [:a:] + q * c) p 0"
> is not yet used --- what is the purpose of it ?

The english Wikipedia defines composition of polynomials as follows:  »A
composition of two polynomials is a polynomial, which is obtained by
substituting a variable of the first polynomial by the second
polynomial.«  I did not try do match that definition mentally against
the Isabelle definition above, but maybe that's it.  You might want to
check it for your own.



PGP available:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.