Zulip Chat Archive

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


Last updated: Dec 20 2023 at 11:08 UTC