refactor(linear_algebra/free_module/pid): move lemmas (#9962)
`linear_algebra/free_module/pid` contains several results not directly related to PID. We move them in more appropriate files.
Except for small golfing and easy generalization, the statements and the proofs are untouched.
Co-authored-by: Johan Commelin <johan@commelin.net>
