mathlib

036527ae - feat(linear_algebra/finite_dimensional): eq_of_le_of_findim_eq (#4005)

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.