leanprover-community/mathlib4

Tracking Issue: Digraph Targets

オープン

#26,771 opened on 2025/07/05

 (7 件のコメント) (1 件のリアクション) (2 人の担当者)Lean (1,592 件のフォーク)github user discovery
good first issuet-combinatorics

Repository metrics

Stars
 (3,869 個のスター)
PR merge metrics
 (30d に merged PR はありません)

説明

This is a list of things related to digraphs that would be nice to have.

  • Weak and strong connectivity.

    • If vertices have equal in-degree and out-degree, then the digraph is weakly connected if and only if it is strongly connected.
    • Robbin's Theorem.
  • Tournaments

    • A tournament has a Hamiltonian path.
    • A tournament has a Hamiltonian cycle If and only if it is strongly connected.

Many of the concepts that already exist in SimpleGraph should be ported to Digraph too. Feel free to add digraph results that you would like to see formalized!

コントリビューターガイド