Stream: math-comp users

Topic: vectType of functions


view this post on Zulip Sylvie Boldo (May 10 2022 at 12:17):

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.

view this post on Zulip Cyril Cohen (May 10 2022 at 12:29):

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?)

view this post on Zulip Sylvie Boldo (May 10 2022 at 12:35):

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.

view this post on Zulip Sylvie Boldo (May 10 2022 at 12:35):

Thanks!


Last updated: Feb 02 2023 at 13:03 UTC