# Re: [isabelle] HOL/Library/Polynomial pcompose

```On 11/28/2013 09:22 AM, Florian Haftmann wrote:
```
```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
```
```
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 *)

```
```Cheers,
Florian
```
```
```
Thank you very much -- suppose, this was the last simple question, a new round of
```questions is on the way ;-)

Walther

```

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