feat(linear_algebra): Matrix inverses for square nonsingular matrices

[Vierkantor]

This is intended as a first step towards defining the generic matrix inverse function. The function nonsing_inv applied to a square matrix A gives its inverse, as long as A.det is invertible. The more general pseudoinverse, which is also defined for singular / non-square matrices, should be defined in terms of this nonsing_inv, but that will be another pull request. I also propose that has_inv (matrix n n R) should be used for the pseudoinverse (but both should take the same value if they are (well-)defined).

The computation of the inverse is done via Cramer's rule, which is definitely not the most optimized way. It should still be computable in a reasonable time, and the correctness proof of Cramer's rule is not too long.

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[ChrisHughes24]

Some comments on the PR. I haven't gone through the whole thing yet.

[ChrisHughes24]

This is the same as quotienting by the subgroup generated by swap i j. This is probably a nicer statement.

[Vierkantor]

I tried rewording the statement, but unfortunately it seems like the original version is easier to work with.

The argument I want to use is that the determinant is a sum adding up to 0 because the term corresponding to σ cancels with the term corresponding to swap i j * σ. Thus, I want to partition the permutations so that the classes are {σ, swap i j * σ}, and then the sum over this class is x + -1 * x + 0 = 0.

Using the quotient of group.closure {swap i j} would then require as a first step showing that the classes are {σ, swap i j * σ}, which was immediate from the original mod_swap definition. (Is there a better way to show quotient_group.left_rel (group.closure {swap i j}) σ τ ↔ (σ = τ ∨ σ = swap i j * τ) than first using group.closure {swap i j} = gpowers (swap i j) = {σ // ∃ k, σ = (swap i j)^k}, then showing (∃ k, σ = (swap i j)^k) ↔ (∃ 0 ≤ k < order_of (swap i j), σ = (swap i j)^k) ↔ (σ = id ∨ σ = swap i j)?) So I don't expect the change is really worth the extra work.

[sgouezel]

mostly cosmetic comments

[sgouezel]

This looks good to me. @ChrisHughes24, do you have more comments?