mathlib3

e0aa9f07 - refactor(linear_algebra/matrix/nonsingular_inverse): clean up (#10175)

refactor(linear_algebra/matrix/nonsingular_inverse): clean up (#10175) This file is a mess, and switches back and forth between three different inverses, proving the same things over and over again. This pulls all the `invertible` versions of these statements to the top, and uses them here and there to golf proofs. The lemmas `nonsing_inv_left_right` and `nonsing_inv_right_left` are merged into a single lemma `mul_eq_one_comm`. The lemma `inv_eq_nonsing_inv_of_invertible` has been renamed to `inv_of_eq_nonsing_inv` This also adds two new lemmas `inv_of_eq` and `det_inv_of`, both of which have trivial proofs.