Re: [Isarmathlib-devel] Re: Polynomial ring

[Slawomir Kolodynski]

Seo, 
Your definition of polynomials excludes the situation where the set of nonzero 
coefficients is empty i.e. the zero polynomial. As a result, the sum of 
polynomials does not have to be a polynomial.
Maybe it is is better to define polynomials as follows:

Support of a function = the set where the function is non-zero

definition
"Supp(f,R,A) \<equiv> {x \<in> domain(f). f`(x) \<noteq> 
TheNeutralElement(R,A)}"

Polynomials = sequences with finite support

definition
"Polynomials(R,A) \<equiv> {f \<in> nat -> R. Supp(f,R,A) \<in> FinPow(nat)"


I would prefer FinPow than Fin, but it will be easier to use Fin as there are 
more theorems about those, in particular that nonempty finite set has a maximum 
(Finite_ZF_1_1T1A).

Slawek