leanprover-community/mathlib4

Tracking Issue: Digraph Targets

开放

#26,771 创建于 2025年7月5日

 (7 条评论) (1 个反应) (2 位负责人)Lean (1,592 个派生)github user discovery
good first issuet-combinatorics

仓库指标

星标
 (3,869 个星标)
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!

贡献者指南