Commit 2023-03-18 23:36 4e7e7009
View on Github →chore(linear_algebra/free_module/basic): golf a proof (#18615) We construct the basis in another file, we may as well use it.
chore(linear_algebra/free_module/basic): golf a proof (#18615) We construct the basis in another file, we may as well use it.