mathlib3

44ab28e3 - refactor(linear_algebra/free_module/finite): move to a new folder (#9821)

refactor(linear_algebra/free_module/finite): move to a new folder (#9821) We move `linear_algebra/free_module/finite` to `linear_algebra/free_module/finite/basic`. We also move two lemmas from `linear_algebra/free_module/finite/basic` to `linear_algebra/free_module/basic`, since they don't need any finiteness assumption on the modules.