[Merged by Bors] - refactor(data/matrix/invertible): more results about invertible matrices

[eric-wieser]

Many results about invertible apply directly to matrices simply by replacing * with matrix.mul.

This also adds some missing lemmas about invertibility of products.

---

[semorrison]

bors merge

[bors[bot]]

:-1: Rejected by label

[eric-wieser]

bors merge

[eric-wieser]

actually

bors d-

This will confuse the dashboard, so I should merge it just before mathport runs

[eric-wieser]

bors r-

[bors[bot]]

Canceled.

[eric-wieser]

Whoops, I guess I forgot about this. Given the likelihood I forget again, let's just put it in.

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests