mathlib3

77e1e3b2 - feat(linear_algebra/nonsingular_inverse): add lemmas about `invertible` (#8201)