feat(Combinatorics/SimpleGraph/Acyclic): a graph is a tree iff it's acyclic and has exactly `n - 1` edges by SnirBroshi · Pull Request #34910 · leanprover-community/mathlib4

SnirBroshi · 2026-02-06T09:59:37Z

This was my white whale for quite some time. Hooray!

depends on: feat(Logic/Equiv/Basic): Sigma over a quotient #34907
depends on: [Merged by Bors] - feat(Data/Sym/Sym2): fromRel equivalence with Sigma over a Quotient #34909

…ent`

…cyclic and has exactly `n - 1` edges

github-actions · 2026-02-06T10:00:46Z

PR summary 8379122c70

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ IsAcyclic.ncard_edgeSet_add_card_connectedComponent
+ IsAcyclic.ncard_edgeSet_add_one_le_card
+ IsTree.ncard_edgeSet_add_one
+ connected_iff_card_connectedComponent_eq_one
+ edgeSetEquivSigmaConnectedComponent
+ exists_isCycle_of_card_le
+ isTree_iff_isAcyclic_and_ncard_edgeSet_add_one_eq_card
+ ofLE
+ sum_connectedComponent_ncard_edgeSet
+ sum_connectedComponent_ncard_supp
+ verticesEquivSigmaConnectedComponent

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 8379122).

+17 new declarations
−0 removed declarations

+RelHom.ofLE
+RelHom.ofLE_apply
+SimpleGraph.IsAcyclic.ncard_edgeSet_add_card_connectedComponent
+SimpleGraph.IsAcyclic.ncard_edgeSet_add_one_le_card
+SimpleGraph.IsTree.ncard_edgeSet_add_one
+SimpleGraph.connected_iff_card_connectedComponent_eq_one
+SimpleGraph.edgeSetEquivSigmaConnectedComponent
+SimpleGraph.edgeSetEquivSigmaConnectedComponent_apply
+SimpleGraph.edgeSetEquivSigmaConnectedComponent_symm_apply_coe
+SimpleGraph.exists_isCycle_of_card_le
+SimpleGraph.isTree_iff_isAcyclic_and_ncard_edgeSet_add_one_eq_card
+SimpleGraph.sum_connectedComponent_ncard_edgeSet
+SimpleGraph.sum_connectedComponent_ncard_supp
+SimpleGraph.verticesEquivSigmaConnectedComponent
+SimpleGraph.verticesEquivSigmaConnectedComponent_apply_fst
+SimpleGraph.verticesEquivSigmaConnectedComponent_apply_snd_coe
+SimpleGraph.verticesEquivSigmaConnectedComponent_symm_apply

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 8379122c70
Reference commit 4efb186f10

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

…arentheses

…n-minus-one

…/simple-graph/tree-iff-acyclic-and-n-minus-one

mathlib-merge-conflicts · 2026-03-20T21:58:26Z

This pull request has conflicts, please merge master and resolve them.

…/simple-graph/tree-iff-acyclic-and-n-minus-one

mathlib-merge-conflicts · 2026-06-10T23:57:13Z

This pull request has conflicts, please merge master and resolve them.

…rel-ndrec-and-equiv-quot

…/simple-graph/tree-iff-acyclic-and-n-minus-one

…n-minus-one

mathlib-dependent-issues · 2026-06-16T10:42:04Z

This PR/issue depends on:

~~feat(Logic/Equiv/Basic): Sigma over a quotient #34907~~
~~[Merged by Bors] - feat(Data/Sym/Sym2): fromRel equivalence with Sigma over a Quotient #34909~~
By Dependent Issues (🤖). Happy coding!

…n-minus-one

amellendijk

Thanks!

Just some minor comments, but this all seems reasonable.

…_of_card_le`

Rida-Hamadani · 2026-07-07T13:13:56Z

  obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic bot_le isAcyclic_bot
  grind [IsTree, Connected, preconnected_iff_reachable_eq_top]

+theorem connected_iff_card_connectedComponent_eq_one :


Is it possible to move this to Connectivity/Connected.lean?

Not without import changes as it doesn't import Nat.card. It is imported in Connectivity/Subgraph.lean and Connectivity/EdgeConnectivity.lean, but they also seem weird.

#40624 will fix the import issues, but no one commented on it yet.

Rida-Hamadani · 2026-07-07T13:21:19Z

  exact Finset.card_lt_card <| by simpa [deleteEdges, edgeFinset]

+/-- An acyclic graph on `n` vertices with `c` connected components has exactly `n - c` edges -/
+theorem IsAcyclic.ncard_edgeSet_add_card_connectedComponent [Finite V] (h : G.IsAcyclic) :


I think the naming is fine, but sometimes while naming we are using the plural connectedComponents such as colorable_iff_forall_connectedComponents, and sometimes not, what do you think is best?

The only uses of the plural seem to be what you mentioned and homOfConnectedComponents. I think colorable_iff_forall_connectedComponents is a typo, and homOfConnectedComponents is probably fine since it's a def.

Good point, fixed in #41648.

docstring periods Co-authored-by: Rida Hamadani <mridahamadani@gmail.com>

…n-minus-one

SnirBroshi added 2 commits February 6, 2026 11:08

feat(Data/Sym/Sym2): fromRel equivalence with Sigma over a `Quoti…

c6ec473

…ent`

feat(Combinatorics/SimpleGraph/Acyclic): a graph is a tree iff it's a…

4980ed5

…cyclic and has exactly `n - 1` edges

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 6, 2026

RelHom.ofLE docstring

cf038ba

SnirBroshi added the t-combinatorics Combinatorics label Feb 6, 2026

SnirBroshi added 18 commits February 7, 2026 01:08

replace Equiv.sigmaQuot with Equiv.sigmaFiberEquiv and tag simps

68b3331

make the type of q explicit in Sigma binders

c29bf8b

replace subst with rfl in rcases

7437183

generalize to fibers

9e8cadc

no need to \comp in the quotients version because we got rid of the p…

353130b

…arentheses

improve Symmetric.comap + Subtype.val spelling

294e917

cosmetic changes

e1df04b

Merge branch 'master' into feature/sym2-fromrel-ndrec-and-equiv-quot

c996f86

Merge branch 'master' into feature/simple-graph/tree-iff-acyclic-and-…

88e2969

…n-minus-one

fix merge

7c870cf

"every" → "an"

1b2c614

remove redundant <|

26389a6

Merge branch 'master' into feature/sym2-fromrel-ndrec-and-equiv-quot

73086cf

fix after the signature of Sym2.hrec changed in master

87bad13

Merge branch 'master' into feature/simple-graph/tree-iff-acyclic-and-…

ad81eb8

…n-minus-one

Merge branch 'feature/sym2-fromrel-ndrec-and-equiv-quot' into feature…

0f9476f

…/simple-graph/tree-iff-acyclic-and-n-minus-one

fix because grind broke somehow

eee507f

might as well

32ebd1a

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 20, 2026

SnirBroshi added 3 commits March 21, 2026 01:42

Merge branch 'master' into feature/sym2-fromrel-ndrec-and-equiv-quot

0ea71f5

Merge branch 'feature/sym2-fromrel-ndrec-and-equiv-quot' into feature…

856c74a

…/simple-graph/tree-iff-acyclic-and-n-minus-one

IsTree.IsAcyclic is deprecated

be182cb

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 20, 2026

SnirBroshi added 3 commits June 2, 2026 07:13

dsimp is now redundant

9bc5dd6

Merge branch 'feature/sym2-fromrel-ndrec-and-equiv-quot' into feature…

4c2f32c

…/simple-graph/tree-iff-acyclic-and-n-minus-one

strange fixes

9e3daec

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 10, 2026

SnirBroshi added 2 commits June 11, 2026 06:25

Merge remote-tracking branch 'upstream/master' into feature/sym2-from…

bc79940

…rel-ndrec-and-equiv-quot

Merge branch 'feature/sym2-fromrel-ndrec-and-equiv-quot' into feature…

058fa64

…/simple-graph/tree-iff-acyclic-and-n-minus-one

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 11, 2026

jt0202 reviewed Jun 12, 2026

View reviewed changes

Comment thread Mathlib/Combinatorics/SimpleGraph/Acyclic.lean Outdated

SnirBroshi added 3 commits June 15, 2026 14:11

Merge branch 'master' into feature/simple-graph/tree-iff-acyclic-and-…

66da04f

…n-minus-one

Nat.card G.edgeSet -> G.edgeSet.ncard

5c98360

G.edgeSet.ncard + 1 = Nat.card V in a finite tree

2ebd30d

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 16, 2026

Merge branch 'master' into feature/simple-graph/tree-iff-acyclic-and-…

16a5dad

…n-minus-one

amellendijk reviewed Jun 18, 2026

View reviewed changes

SnirBroshi added 7 commits June 18, 2026 17:53

card_edgeSet -> ncard_edgeSet in names

e952ebd

delete card_vert_le_ncard_edgeSet_isAcyclic

fbff91b

rename card_vert_le_ncard_edgeSet_exists_isCycle -> `exists_isCycle…

ea26511

…_of_card_le`

more name fixes

43c05db

Quot.mk G.Reachable -> G.connectedComponentMk

87fd089

IsTree.ncard_edgeSet_add_one follows directly from the finset version

f60f58a

golf isTree_iff_isAcyclic_and_ncard_edgeSet_add_one_eq_card

fc3fa5a

mathlib-triage Bot assigned b-mehta Jun 26, 2026

Rida-Hamadani reviewed Jul 7, 2026

View reviewed changes

SnirBroshi and others added 5 commits July 11, 2026 22:33

Apply suggestions from code review

7eabf4a

docstring periods Co-authored-by: Rida Hamadani <mridahamadani@gmail.com>

Merge branch 'master' into feature/simple-graph/tree-iff-acyclic-and-…

50081fe

…n-minus-one

more docstring periods

8846957

small golf to ncard_edgeSet_add_card_connectedComponent

f2906dc

extract the summations of connected component sizes to lemmas

8379122

Uh oh!

Conversation

SnirBroshi commented Feb 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Feb 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8379122c70

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-merge-conflicts Bot commented Mar 20, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Jun 10, 2026

Uh oh!

Uh oh!

mathlib-dependent-issues Bot commented Jun 16, 2026

Uh oh!

amellendijk left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Rida-Hamadani Jul 7, 2026

Choose a reason for hiding this comment

Uh oh!

SnirBroshi Jul 11, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Rida-Hamadani Jul 7, 2026

Choose a reason for hiding this comment

Uh oh!

SnirBroshi Jul 11, 2026

Choose a reason for hiding this comment

Uh oh!

Rida-Hamadani Jul 12, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

SnirBroshi commented Feb 6, 2026 •

edited

Loading

github-actions Bot commented Feb 6, 2026 •

edited

Loading