Hello! I am looking for getting a vectTYpe of functions. In vector, I found one for functions from a finType into a ring but I am looking for a more generic vectype of functions (from ring to ring), to get a vector space of functions from Z to Z for instance.

Is there a way or should I define the Canonical myself?

Thanks.

Sylvie Boldo said:

Hello! I am looking for getting a vectTYpe of functions. In vector, I found one for functions from a finType into a ring but I am looking for a more generic vectype of functions (from ring to ring), to get a vector space of functions from Z to Z for instance.

Is there a way or should I define the Canonical myself?

Thanks.

This does not exist in mathcomp at the moment, since the choice has been made a long time ago to have only finite dimensional vector spaces, in order to preserve the decidability or computability of many things (e.g. completing a basis, etc). The best you can get as of now is a module type on a field, i.e. `lmodType`

in mathcomp (and its extensions with the norm etc in mathcomp-analysis) . (BTW, I'm not sure which vector space structure you hope to get on functions from Z to Z, did you mean from Z to R for example?)

I was thinking about R->R (to get polynomials for instance) but the definition of R was not important here so I explained it with Z->Z.

Thanks!

Last updated: Feb 02 2023 at 13:03 UTC