Skip to content

feat(Combinatorics/SimpleGraph/Acyclic): a graph is a tree iff it's acyclic and has exactly n - 1 edges#34910

Open
SnirBroshi wants to merge 53 commits into
leanprover-community:masterfrom
SnirBroshi:feature/simple-graph/tree-iff-acyclic-and-n-minus-one
Open

feat(Combinatorics/SimpleGraph/Acyclic): a graph is a tree iff it's acyclic and has exactly n - 1 edges#34910
SnirBroshi wants to merge 53 commits into
leanprover-community:masterfrom
SnirBroshi:feature/simple-graph/tree-iff-acyclic-and-n-minus-one

extract the summations of connected component sizes to lemmas

8379122
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Jul 11, 2026 in 1m 12s