Does anyone know a good starting point to try Lean for Linear Algebra?
https://leanprover-community.github.io/mathematics_in_lean/i...
It doesn't get to linear algebra till chapter 9, and it tends to be cumulative, but you could try the first 4 chapters to get the basics and jump ahead to see how you get on