Commit 2021-02-04 12:05 97781b9a

chore(linear_algebra/std_basis): move std_basis to a new file (#6020) linear_algebra/basic is very long. This reduces its length by about 5%. Authorship of the std_basis stuff seems to come almost entirely from 10a586b1d82098af32e13c8d8448696022132f17. None of the lemmas have changed, and the variables are kept in exactly the same order as before.