mathlib3

d90448c6 - chore(linear_algebra/*): changes to finsupp_vectorspaces and move module doc dual (#6516)

chore(linear_algebra/*): changes to finsupp_vectorspaces and move module doc dual (#6516) This PR does the following: - move the module doc of `linear_algebra.dual` so that it is recognised by the linter. - add `ker_eq_bot_iff_range_eq_top_of_findim_eq_findim` to `linear_algebra.finite_dimensional`, this replaces `injective_of_surjective` in `linear_algebra.finsupp_vectorspaces` - remove `eq_bot_iff_dim_eq_zero` from `linear_algebra.finsupp_vectorspaces`, this already exists as `dim_eq_zero` in `linear_algebra.finite_dimensional` - changed `cardinal_mk_eq_cardinal_mk_field_pow_dim` and `cardinal_lt_omega_of_dim_lt_omega` to assume `finite_dimensional K V` instead of `dim < omega`. - renamed `cardinal_lt_omega_of_dim_lt_omega` to `cardinal_lt_omega_of_finite_dimensional` since the assumption changed. - provided a module doc for `linear_algebra.finsupp_vectorspaces` which should remove `linear_algebra.*` from the style exceptions file. This file should probably be looked at again by someone more experienced in the linear_algebra part of the library. It seems to me that most of the statements in this file in fact would better fit in other files. Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>