Matrix Rings

[Alizter]

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

• 1956

• 1957

• 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]

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.

[Alizter]

@jdchristensen Are we ready to merge?

[jdchristensen]

Yes, LGTM.