Possible Project on Linear Algebra

[AR-MA210]

I suggest the following project:

Implement basic linear algebra in Idris (checking with proofs for linear dependence, finding eigenvalues and eigenvectors with proof, diagonalizing matrices, etc).

I think this project is sufficiently mathematical to be interesting and also does not require too many definitions to get started on.

Would this be a good idea?

--Abishek

[siddhartha-gadgil]

It is certainly a good project. Linear equations is the first step for this. It will take work though, since eigenvalues will need reals, or at least algebraic numbers, which is a project in itself.