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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de




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