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: May 13 2021 at 21:12 UTC