vector_space vs module

Stream: new members

[David Chanin]

I'm trying to follow along the xena linear algebra lecture (https://www.youtube.com/watch?v=cp1AihuYr9k), and it uses vector_space in the start of the video. When I try to copy the code there, vector_space doesn't exist. But looking at the docs it looks like module means the same thing? But then the definition of module doesn't mention field like vector_space seems to from old mathlib versions. Are these really the same? Or is there another import where I can find the proper vector_space?

[Patrick Massot]

Yes, you can assume module means vector space.

[Patrick Massot]

If you don't know what is a module in math, simply think this is our weird spelling for "vector space".

[David Chanin]

:+1: OK I'll assume it means that moving forward!