Commit 2021-10-23 14:30 29c72664

refactor(linear_algebra/matrix/nonsingular_inverse): use ring.inverse in matrix.has_inv (#9863) This makes some of the proofs a little shorter. Independently, this removes an assumption from matrix.transpose_nonsing_inv. This adds the missing units.is_unit_units_mul to complement the existing units.is_unit_mul_units, even though it ultimately was not used in this PR. This removes the def matrix.nonsing_inv in favor of just using has_inv.inv directly. Having two ways to spell the same thing isn't helpful here.