chore(linear_algebra/free_module/basic): tidy up (#15956)
This generalizes a few free instances to not assume the same ring appears twice, notably `module.free R (ι →₀ R)` to `module.free R (ι →₀ M)` and `module.free R (matrix m n R)` to `module.free R (matrix m n M)`.
This renames `module.free.pi.free`, a special case of `module.free.pi`, to `module.free.function`.
It also renames `module.free.finsupp.free` to `module.free.finsupp`.
In order to make this change we relax the typeclasses in `finsupp.basis` from rings to semirings.
We make the same relaxation on `module.free.pi`, which results in us running into the same typeclass search bug that already occurs for `module.finite`.
Finally, at the request of the new linter this changes `fintype` assumptions to `finite`.
