Commit 2020-08-31 22:41 036527ae

feat(linear_algebra/finite_dimensional): eq_of_le_of_findim_eq (#4005) Add a variant of eq_top_of_findim_eq, where instead of proving a submodule equal to ⊤, it's shown equal to another finite-dimensional submodule with the same dimension that contains it. The two lemmas are related by the comap_subtype lemmas, so the proof is short, but it still seems useful to have this form.