Re: [isabelle] HOL/Library/Polynomial pcompose
On 11/28/2013 09:22 AM, Florian Haftmann wrote:
Am 23.11.2013 15:24, schrieb Walther Neuper:
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.
value "pcompose [:1,1,1::int:] [:1,1::int:]" --"Poly [3, 3, 1]"
(*substitute for x in (1+x+x^2) by (1+x) = 1 + (1+x) + (1+x)^2 = 3 + 3x + x^2 *)
Thank you very much -- suppose, this was the last simple question, a new
questions is on the way ;-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and