Theorem SimpleGraph.exists_ne_odd_degree_of_exists_odd_degree

Modification history

2023-03-23 14:47
Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean
feat: Port Combinatorics.SimpleGraph.DegreeSum (#2895)
Added SimpleGraph.exists_ne_odd_degree_of_exists_odd_degreeView on Github →