vector space

Stream: Is there code for X?

[Alex Kontorovich]

Is there a reason the linear algebra file doesn't define vector space? I see things like

def basis.of_vector_space (K : Type u_4) (V : Type u) [division_ring K] [add_comm_group V] [module K V]

but should the division_ring, module etc be called vector_space that extends these?

[Adam Topaz]

This is a historical artifact. We did have a vector_space class a while ago, which was dropped. The idea is that one should always use module.

[Violeta Hernández]

This is also the reason while we have a lot of theorems with dim on the name that actually talk about rank

[Violeta Hernández]

Someone should get to doing these renames someday...

[Eric Wieser]

I tried to do that rename once but got stuck lost interest because of some name conflicts

[Kevin Buzzard]

@Anne Baanen suggested localized "notation `vector_space` := module" in vector_space here.