Re: [isabelle] HOL/Library/Polynomial pcompose
Am 23.11.2013 15:24, schrieb Walther Neuper:
> the definition
> definition pcompose :: "'a::comm_semiring_0 poly => 'a poly => 'a poly"
> "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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and