There is a large library of mathematics formalized in lean called mathlib. There are graphs for the module dependencies, but I haven't seen any at the level of

There is a large library of mathematics formalized in lean called mathlib. There are graphs for the module dependencies, but I haven't seen any at the level of definitions (including lemmas and theorems).