This is a formalization of Axler, Linear Algebra Done Right, in Lean 4 with Mathlib, using the 4th edition of Axler, freely available at Axler's site
Because Mathlib treats linear algebra in full generality at a graduate level, it takes some work to apply down to the level of Linear Algebra Done Right, by translating the more general concepts down to the undergraduate level. This repository attempts to document the concepts necessary to understand the application of Mathlib concepts to the language of Axler.
Very much a work in progress. Collaboration welcome at the Zulip
Chapter 1 of Linear Algebra Done Right in Lean 4 has been done a few times before
Martin C Martin did the chapter content (not the exercises) https://github.com/martincmartin/linear_algebra_done_right/
Tyler Hanks did a re-implementation (no Mathlib): https://github.com/tylerhanks/leanear-algebra