mathlib

fbfe26dc - feat(linear_algebra/finite_dimensional): `dim_add_le_dim_add_dim` (#16301)

feat(linear_algebra/finite_dimensional): `dim_add_le_dim_add_dim` (#16301) Add a `finrank` version of a lemma that already exists for `module.rank`. The proof is exactly the same as the proof of the `module.rank` version, and, as with the previous `dim_sup_add_dim_inf_eq` lemma that it uses, so is the name (but in the `submodule` namespace in the case of the `finrank` versions).