subspace

Stream: maths

[Johan Commelin]

We recently unified semimodule, module, and vector_space into module. But I just noticed that subspace still exists (and assume the coefficient ring to be a field). Do we want to keep it around, or shall we just use submodule everywhere?