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`

Author: Vierkantor