Commit 2021-11-08 08:27 e0aa9f07

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.