mathlib

244285c9 - feat(linear_algebra/free_module): add instances (#9087)

feat(linear_algebra/free_module): add instances (#9087) We add some `module.finite` instances. These are in the `linear_algebra/free_module.lean` files since they concern free modules. From LTE Co-authored-by: Johan Commelin <johan@commelin.net>