mathlib3

4091f72b - refactor(linear_algebra/free_module): split in two files (#9407)

refactor(linear_algebra/free_module): split in two files (#9407) We split `linear_algebra/free_module` in `linear_algebra/free_module/basic` and `linear_algebra/free_module/finite`, so one can work with free modules without having to import all the theory of dimension.