Mathlib v3 is deprecated. Go to Mathlib v4

Theorem simple_graph.exists_ne_odd_degree_of_exists_odd_degree

Modification history

2021-01-27 18:19
src/combinatorics/simple_graph/degree_sum.lean
feat(data/fintype/basic): make subtype_of_fintype computable (#5919) …
Modified simple_graph.exists_ne_odd_degree_of_exists_odd_degreeView on Github →
2020-12-11 01:46
src/combinatorics/simple_graph/degree_sum.lean
feat(combinatorics/simple_graph/degree_sum): degree-sum formula and handshake lemma (#5263) …
Added simple_graph.exists_ne_odd_degree_of_exists_odd_degreeView on Github →