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