leanear-algebra Formalizing Sheldon Axler's Linear Algebra Done Right using Lean (Leanear Algebra Done Right).