monlib (m(on)ath lean library) (monlib + mathlib3) Still a work in progress (WIP). This is an ongoing attempt at the formalisation of some random stuff on non-commutative graph theory in Lean3. TODO: Will include a thorough table of contents soon.