feat(linear_algebra/free_module): add instances (#9072)
From LTE.
We prove that `M →ₗ[R] N` is free if both `M` and `N` are finite and free. This needs the quite long result that for a finite and free module any basis is finite.
Co-authored with @jcommelin
