mathlib3

5f45c0c6 - feat(linear_algebra/finite_dimensional): finite-dimensional submodule lemmas / instances (#4128)

feat(linear_algebra/finite_dimensional): finite-dimensional submodule lemmas / instances (#4128) Add the lemma that a submodule contained in a finite-dimensional submodule is finite-dimensional, and instances that allow type class inference to show some infs and sups involving finite-dimensional submodules are finite-dimensional. These are all useful when working with finite-dimensional submodules in a space that may not be finite-dimensional itself. Given the new instances, `dim_sup_add_dim_inf_eq` gets its type class requirements relaxed to require only the submodules to be finite-dimensional rather than the whole space. `linear_independent_iff_card_eq_findim_span` is added as a variant of `linear_independent_of_span_eq_top_of_card_eq_findim` for vectors not necessarily spanning the whole space (implemented as an `iff` lemma using `findim_span_eq_card` for the other direction).