basic): golf a proof (#18615)

Commit

2 years ago

chore(linear_algebra/free_module/basic): golf a proof (#18615) We construct the basis in another file, we may as well use it.

Author

eric-wieser

Parents