leanprover-community/mathlib4

Tracking Issue: Digraph Targets

開放

#26,771 建立於 2025年7月5日

 (7 則留言) (1 個反應) (2 位負責人)Lean (1,381 個分叉)github user discovery
good first issuet-combinatorics

倉庫指標

星標
 (3,405 顆星)
PR 合併指標
 (30 天內沒有已合併 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!

貢獻者指南