Commit 2021-03-05 11:27 d90448c6

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.