Commit 2023-03-23 14:47 d353a387

View on Github →

feat: Port Combinatorics.SimpleGraph.DegreeSum (#2895)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

added theorem SimpleGraph.Dart.edge_fiber

added theorem SimpleGraph.dart_card_eq_sum_degrees

added theorem SimpleGraph.dart_card_eq_twice_card_edges

added theorem SimpleGraph.dart_edge_fiber_card

added theorem SimpleGraph.dart_fst_fiber

added theorem SimpleGraph.dart_fst_fiber_card_eq_degree

added theorem SimpleGraph.even_card_odd_degree_vertices

added theorem SimpleGraph.exists_ne_odd_degree_of_exists_odd_degree

added theorem SimpleGraph.odd_card_odd_degree_vertices_ne

added theorem SimpleGraph.sum_degrees_eq_twice_card_edges