Commit 2022-11-11 20:43 667de7b2

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