mathlib3

24901dde - feat(linear_algebra/free_module/rank): rank of free modules (#9810)

feat(linear_algebra/free_module/rank): rank of free modules (#9810) This file contains a basic API for the rank of free modules. We will add the results for finite free modules in a future PR.