Commit 2021-10-26 07:25 717de02d
View on Github →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.