mathlib3

2c0b43d9 - feat(combinatorics/simple_graph/degree_sum): degree-sum formula and handshake lemma (#5263)

feat(combinatorics/simple_graph/degree_sum): degree-sum formula and handshake 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>