WARNING: Please do not open a pull request in this repository.
This is not the relevant repository to contribute to Mathematics in Lean. This repository is cloned by people who want to study the book. It is automatically created from the source repository which can be found at https://github.com/avigad/mathematics_in_lean_source and where you can open a pull-request.