mathlib3

90418df5 - feat(linear_algebra/finite_dimensional): `finite_dimensional_iff_of_rank_eq_nsmul` (#13357)

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.