I am starting to understand Lean 4, but I feel a bit overwhelmed by the amount of dependencies for most files in Mathlib. To become more familiar, particularly with the module typeclass, I decided to read through the Mathlib files from group defs to modules. It was helpful, but I still feel lost. What are the must-read Mathlib files for understanding a lot of the further work, in some or any field? Is there anything neat I should look into? (My current field of study is random geometry, which requires a lot of functional and complex analysis, measure theory, random graph theory, stochastic calculus, etc. Similar ideas would be nice to look into as well.)
$\begingroup$
$\endgroup$
Add a comment
|