mathlib3

667de7b2 - chore(linear_algebra): split `finrank` results that don't depend on `finite_dimensional` (#17473)

chore(linear_algebra): split `finrank` results that don't depend on `finite_dimensional` (#17473) This PR splits up `linear_algebra/finite_dimensional.lean` by moving the definition of `finrank` and all the results that don't require a `[finite_dimensional K V]` hypothesis to a new file `linear_algebra/finrank.lean`. The purpose of this change is to insert `linear_algebra/free_module/finite.lean` in between `linear_algebra/finrank.lean` and `linear_algebra/finite_dimensional.lean`, as discussed in the module docs for `linear_algebra/free_module/finite.lean` and in #17401. In order to avoid `finite_dimensional` I also reworked some proofs, for which I added new lemmas `finrank_le_of_dim_le`, `finrank_lt_of_dim_lt` and `dim_lt_of_finrank_lt`. The following lemmas have different proofs: * `finrank_eq_card_basis` * `finrank_self` * `finrank_fintype_fun_eq_card` * `finrank_bot` * `finrank_span_eq_card` * `finrank_span_set_eq_card` * `subalgebra.finrank_bot` * `finrank_span_le_card` * `nontrivial_of_finrank_pos`