Commit 2026-10-17 16:48 06786687

View on Github →

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

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

added theorem SimpleGraph.IsAcyclic.ncard_edgeSet_add_card_connectedComponent

added theorem SimpleGraph.IsAcyclic.ncard_edgeSet_add_one_le_card

added theorem SimpleGraph.IsTree.ncard_edgeSet_add_one

added theorem SimpleGraph.exists_isCycle_of_card_le

added theorem SimpleGraph.isAcyclic_iff_forall_not_isCycle

added theorem SimpleGraph.isTree_iff_isAcyclic_and_ncard_edgeSet_add_one_eq_card

added theorem SimpleGraph.not_isAcyclic_iff_exists_isCycle

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

added theorem SimpleGraph.ConnectedComponent.encard_supp

added theorem SimpleGraph.ConnectedComponent.ncard_supp

deleted theorem SimpleGraph.Preconnected.subsingleton_connectedComponent

added theorem SimpleGraph.card_connectedComponent_eq_one_iff

added def SimpleGraph.edgeSetEquivSigmaConnectedComponent

added theorem SimpleGraph.isEmpty_connectedComponent_iff

added theorem SimpleGraph.nonempty_connectedComponent_iff

added theorem SimpleGraph.subsingleton_connectedComponent_iff

added theorem SimpleGraph.sum_connectedComponent_ncard_edgeSet

added theorem SimpleGraph.sum_connectedComponent_ncard_supp

added def SimpleGraph.verticesEquivSigmaConnectedComponent

Modified Mathlib/Order/RelIso/Basic.lean