Commit 2022-08-30 09:26 fbfe26dc

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