A Lean formalisation of parts of Martin Liebeck's "A concise introduction to pure mathematics".
A Xena summer project.
This is a Lean 3 project. Assuming you have already installed Lean and its supporting tools you can install this Lean project with
leanproject get ImperialCollegeLondon/m1fexplained
Right now, feel free to make pull requests adding either statements of, or solutions to, the exercises. Feel free to also write in English in the comments what the exercises say.