The Matrix Cookbook, using Lean's mathlib
This repository aims to provide the lemmas in The Matrix Cookbook (November 15, 2012) as proofs in the Lean theorem prover.
Ideally, every proof in this repository should be a reference to a single lemma in Mathlib, the maths library for lean.
The progress bar below shows the state of this repository; green represents lemmas which are proven, yellow lemmas which are stated, red lemmas which are ready to be stated, and dark red for entire missing sections. Clicking on the progress bar will take you to a version that links to each lemma.
