Lineare Algebra in Lean