Vector space syntax

Stream: new members

[Kirby Sikes]

If I have a discrete field F, and I want to talk about the n-dimensional vector space (for some nat n) on that field, how do I do that? I assume it uses discrete_field.to_vector_space, but I don't understand the syntax.

[Kevin Buzzard]

This question (which I don't know the answer to without looking in the library) is somehow a great indicator of exactly how poor our documentation for mathematicians is.

[Kevin Buzzard]

I might be tempted just to define it as fin n -> F and import something like algebra.pi_instances which probably gives it the vector space structure

[Kirby Sikes]

Thanks.