Vector space with basis

[Tragicus]

#1718 will introduce the notion the max norm of a vector space, which depends on a choice of basis. As per earlier discussions, we should introduce a structure for vector space equipped with a basis.

[affeldt-aist]

Is this issue completely addressed by the merge of PR #1718 ?

[Tragicus]

No, it is an example of a case where we would have liked to have the structure.