isarmathlib-devel
[Top][All Lists]

## Re: [Isarmathlib-devel] Re: Polynomial ring

 From: Slawomir Kolodynski Subject: Re: [Isarmathlib-devel] Re: Polynomial ring Date: Thu, 12 Jun 2008 15:31:43 -0700 (PDT)

```Seo,

Couple of remarks on your first version:

I would use TheNeutralElement(R,A) instead of Z in
your definition of the set of of polynomials over R.
Something like:

definition
"PolynomialsOver(R,A) \<equiv>
{x \<in> nat -> R . HasAmaximum(Le, {n \<in> nat. x(n)
\<noteq> TheNeutralElement(R,A)}"

This is not very important, but it is a little closer
to what we think polynomials are.

I suggest you consider defining polynomial addition as
a restriction of the lift of the addition to the set
of polynomials. The lift of the addition to a function
space over nat is the pointwise addition of infinite
sequences, then you restrict it to the subset of
polynomials. Something like

definition
restrict(A {lifted to function space over} nat,
PolynomialsOver(R,A)\<times>PolynomialsOver(R,A))"

This should make it easier to show that polynomials
form a group.

See func_ZF.thy for about lifting and restricting of
associative and commutative operations.
More remarks later.

Slawek

This will make it easier to show that polynomials form
a group.

http://savannah.nongnu.org/projects/isarmathlib
Library of Formalized Mathematics for Isabelle/Isar (ZF Logic)

```