Commit 2023-08-01 12:59 4d415323

View on Github →

feat: Number of edges of a tree (#5918) Port/review of [mathlib#18638](https://github.com/leanprover-community/mathlib/pull/18638) directly to Mathlib4.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

added theorem SimpleGraph.IsTree.card_edgeFinset

added theorem SimpleGraph.IsTree.existsUnique_path

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

added theorem SimpleGraph.Walk.IsPath.tail

added inductive SimpleGraph.Walk.Nil

added theorem SimpleGraph.Walk.adj_sndOfNotNil

added theorem SimpleGraph.Walk.cons_support_tail

added theorem SimpleGraph.Walk.cons_tail_eq

added theorem SimpleGraph.Walk.edge_firstDart

added def SimpleGraph.Walk.firstDart

added theorem SimpleGraph.Walk.length_tail_add_one

added theorem SimpleGraph.Walk.nil_copy

added theorem SimpleGraph.Walk.nil_iff_length_eq

added theorem SimpleGraph.Walk.nil_iff_support_eq

added theorem SimpleGraph.Walk.nil_nil

added def SimpleGraph.Walk.notNilRec

added theorem SimpleGraph.Walk.not_nil_cons

added theorem SimpleGraph.Walk.not_nil_iff

added theorem SimpleGraph.Walk.not_nil_of_ne

added def SimpleGraph.Walk.sndOfNotNil

added def SimpleGraph.Walk.tail