Linear Algebra is a mess

sharmaeklavya2 / theoremdep-source

Source files for TheoremDep - a theorem dependency tracker

https://sharmaeklavya2.github.io/theoremdep/

19 stars 1 forks source link

Linear Algebra is a mess #1

Open sharmaeklavya2 opened 4 years ago

sharmaeklavya2 commented 4 years ago

In an effort to be as formal and general as possible, I wrote theorems in the Linear Algebra section in a way that makes them very difficult to use and their proofs are complicated and the dependencies aren't arranged neatly. Of course, I realized this after the blunder was done.

I don't have the time to fix this, but I'll gladly help anyone else who wants to clean this up.

sharmaeklavya2 commented 2 years ago

Progress on fixing:

[ ] Vector Spaces
[ ] Linear Transformation
[x] Inner Product Spaces
[ ] Matrices
[ ] System of Linear Equations
[ ] Eigenvectors