Commit 2022-05-02 15:58 90418df5
View on Github →feat(linear_algebra/finite_dimensional): finite_dimensional_iff_of_rank_eq_nsmul (#13357)
If V has a dimension that is a scalar multiple of the dimension of W, then V is finite dimensional iff W is.