Commit 2021-02-05 15:46 bd38c5ff
View on Github →chore(linear_algebra): move is_basis_std_basis to std_basis.lean (#6054)
This is a follow-up to #6020 which moved std_basis to a new file: now move results from basis.lean to that same file.
CC @eric-wieser