*To*: Walther Neuper <wneuper at ist.tugraz.at>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] HOL/Library/Polynomial pcompose*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 28 Nov 2013 09:22:02 +0100*In-reply-to*: <5290BAB4.6020108@ist.tugraz.at>*Organization*: TU Munich*References*: <5290BAB4.6020108@ist.tugraz.at>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:24.0) Gecko/20100101 Thunderbird/24.1.1

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

**Follow-Ups**:**Re: [isabelle] HOL/Library/Polynomial pcompose***From:*Walther Neuper

**References**:**[isabelle] HOL/Library/Polynomial pcompose***From:*Walther Neuper

- Previous by Date: Re: [isabelle] Order of Serialization for code_printing code_module
- Next by Date: Re: [isabelle] export_code doesn't define Trueprop for False
- Previous by Thread: [isabelle] HOL/Library/Polynomial pcompose
- Next by Thread: Re: [isabelle] HOL/Library/Polynomial pcompose
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list