Formalising non-commutative graph theory in Lean 4.
Previous version: monlib in Lean 3
Formalising non-commutative graph theory in Lean