-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(combinatorics/simple_graph/degree_sum): degree-sum formula and handshake lemma #5263
Conversation
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
…ity/mathlib into simple_graphs3 grabbing commits from github
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
…ity/mathlib into simple_graphs3 implementing changes
Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
…ity/mathlib into simple_graphs3 fdsjka
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ity/mathlib into simple_graphs3 pulling new commits
Yeah I think this new definition to the |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think the filename could be a little more general and make contact with the names of its declarations, maybe degree_sum.lean
?
I made a few name suggestions; apologies if I missed some of the renamings.
LGTM once the TODO_move section is put in the right spot.
I changed it to
I put them in |
I'm doing this from my laptop, which doesn't have lean installed, so this might take another commit if I made a mistake.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
bors r+
…andshake lemma (#5263) Adds the theorem that the sum of the degrees of the vertices of a simple graph is twice the number of edges. Also adds corollaries like the handshake lemma, which is that the number of odd-degree vertices is even. The corollary `exists_ne_odd_degree_if_exists_odd` is in anticipation of Sperner's lemma. Co-authored-by: agusakov <39916842+agusakov@users.noreply.github.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Adds the theorem that the sum of the degrees of the vertices of a simple graph is twice the number of edges. Also adds corollaries like the handshake lemma, which is that the number of odd-degree vertices is even.
The corollary
exists_ne_odd_degree_if_exists_odd
is in anticipation of Sperner's lemma.