Commit 2020-09-14 15:35 5f45c0c6

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).