Matrix Rings

[Alizter]

This PR is a draft until the following dependencies are merged:

• abstract out some idioms for dealing with decidable types #1956
• more theory about lists #1957
• finite sums of ring elements #1959

In this PR we define matrices together with:

• The abelian group structure of matrices over a ring (could be an abelian group but no need for now).
• The ring structure of matrices given by matrix multiplication
• Transposed matrices and some basic properties
• Matrix minors and some basic properties
• Trace of a matrix and some basic properties

There is also a test file demonstrating how matrices can be built and used in practice. We also test some examples there too.

I have some more work on the determinant, however this requires some more work on finite types such as sums over an arbitrary finite type and permutations. We can define the determinant using the rule with minors however it is not easy to prove properties about it. My future attempt will be to define it as a sum of products with sign given by the permutation we sum over.

[jdchristensen]

I read just the first half of this.

We're probably going to want a vector type (lists of a fixed length). So one could define m x n matrices to be a vector of vectors of elements of R. Then you don't have to track lengths, and various things you want to prove about matrices would follow from the corresponding facts about vectors (e.g. truncatedness, the abelian group structure, indexing, entry_Build_Matrix, path_matrix, etc.) Basically everything that operates on a matrix "pointwise" will be easier to prove for 1-d vectors than 2-d arrays, and will extend, and this covers almost exactly half of the file Matrix.v.

So I think it will be cleaner to first define vectors over a ring R, and then reuse that in this file.

[jdchristensen]

So I think it will be cleaner to first define vectors over a ring R, and then reuse that in this file.

This is also the free module of a given rank, so it will be something we need anyways.

[Alizter]

@jdchristensen I've introduced a Vector.v file concerning lists of a specified length. We could generalise this data structure in the future if we ever have the need, but for now I only care about linear algebra so I will keep it in the algebra library.

In order for the module structure to be inherited for matrices I had to generalise the R-module structure on vectors by supposing the elements where from R-modules themselves rather than just R.

Most of the matrix multiplication proofs were left unchanges, although sometimes the entry_Build_Matrix lemma doesn't work since the operations are about Vector.entry. This is solved by also rewriting with entry_Build_Vector. It might even be worth to get rid of entry_Build_Matrix entirely.

[jdchristensen]

I think using Vector improved things a lot. I'm about to push some small changes.

[Alizter]

@jdchristensen Are we ready to merge?

[jdchristensen]

Yes, LGTM.