Commit 2020-12-11 01:46 2c0b43d9

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.