This project contains a Lean file LeanDerivedCategories.lean which accompanies the paper Formalization of derived categories in Lean/Mathlib by Joël Riou. This file follows the same structure as the paper and is meant to facilitate the cross-references between the mathematical text and the corresponding definitions in the Lean code, which is part of the mathlib branch jriou_localization.
- Get a working Lean installation
git clone https://github.com/joelriou/lean-derived-categories.gitcd lean-derived-categorieslake exe cache get- launch
VS codeon this directory