mathlib

62e13643 - chore(linear_algebra/nonsingular_inverse): `matrix.nonsing_inv` no longer requires base ring to carry `has_inv` instance (#3136)