mathlib3
feat(combinatorics.simple_graph.acyclic): Trees are maximal acyclic, resp. minimal connected graphs.
#18685
Open

feat(combinatorics.simple_graph.acyclic): Trees are maximal acyclic, resp. minimal connected graphs. #18685

bottine wants to merge 30 commits into master from bottine/simple_graph/trees_min_max2
bottine
bottine init
fcafc94d
bottine acyclic and friends using from_edge_set
6a52449c
bottine slow
041fc2b0
bottine still slow
4b8aebec
bottine what was previously called `walk.split_along_set`
800755b3
bottine acyclic now doesn't use delete_edges anymore
950c44b2
bottine more from edge set
0ac8d80d
bottine more lemmas (Kyle's code)
7b50e494
bottine Kyle's suggestions
db2f1877
bottine Yael's suggestion
a4b1c856
bottine merge
8cd77976
bottine more stuff
f0917de9
bottine more stuff
8a79db9c
bottine no sorry but lots of cleanup to do
3038c16a
bottine cleaning up
e61776e1
bottine cleaning up
4ab9f8e3
bottine cleaning up
91c8d29f
bottine error
aa2b38be
bottine error
c9292bd5
bottine error
370ca955
bottine mathlib lint
bf519f1e
bottine externalize lemmas
fdb47d9a
bottine externalize lemmas
d5c9d344
bottine externalize lemmas
41b37567
bottine externalize lemmas
32a2fe1f
bottine cleanup
8a9ba139
bottine mathlib lint
4e1a594e
bottine merge master
7d78430b
bottine ok
7ade8bea
bottine less sorry
20ac6d4d
bottine bottine added WIP
bottine bottine added t-combinatorics
bottine bottine requested a review 2 years ago
bottine bottine marked this pull request as draft 2 years ago
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
Milestone