The canonical introduction is Mathematics in Lean https://leanprover-community.github.io/mathematics_in_lean/index.html https://leanprover-community.github.io/

The canonical introduction is Mathematics in Lean https://leanprover-community.github.io/mathematics_in_lean/index.html 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