## Stream: new members

### Topic: Vector space syntax

#### Kirby Sikes (Feb 25 2020 at 22:39):

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 (Feb 25 2020 at 22:58):

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 (Feb 25 2020 at 23:03):

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 (Feb 25 2020 at 23:05):

Thanks.

Last updated: May 13 2021 at 21:12 UTC