/LADR

Formalizing "Linear Algebra Done Right" using Lean

Primary LanguageLean

LADR

The goal of this project is to identify the corresponding definitions and theorems from the book "Linear Algebra Done Right" within Mathlib. If there are no direct counterparts in Mathlib, the aim is to utilize as many existing definitions and proofs from Mathlib as possible.

WIP

Linear Algebra Done Right (Third Edition)

Chapter 1

Chapter 2

Chapter 3