mathlib

722b3b15 - refactor(data/matrix/invertible): more results about invertible matrices (#19204)

refactor(data/matrix/invertible): more results about invertible matrices (#19204) Many results about `invertible` apply directly to matrices simply by replacing `*` with `matrix.mul`. This also adds some missing lemmas about invertibility of products.