mathlib
465d4301 - chore(linear_algebra/free_module/rank): golf a slow proof (#18804)

Commit
2 years ago
chore(linear_algebra/free_module/rank): golf a slow proof (#18804) We already do all the work for this when constructing the basis elsewhere.
Author
Parents
Loading