Commit 2023-03-02 08:11 ed9eca59

View on Github →

feat: Port Combinatorics.SimpleGraph.Trails (#2574)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Trails.lean

added theorem SimpleGraph.Walk.IsEulerian.card_filter_odd_degree

added theorem SimpleGraph.Walk.IsEulerian.card_odd_degree

added theorem SimpleGraph.Walk.IsEulerian.edgesFinset_eq

added theorem SimpleGraph.Walk.IsEulerian.even_degree_iff

added def SimpleGraph.Walk.IsEulerian.fintypeEdgeSet

added theorem SimpleGraph.Walk.IsEulerian.isTrail

added theorem SimpleGraph.Walk.IsEulerian.mem_edges_iff

added def SimpleGraph.Walk.IsEulerian

added def SimpleGraph.Walk.IsTrail.edgesFinset

added theorem SimpleGraph.Walk.IsTrail.even_countp_edges_iff

added theorem SimpleGraph.Walk.IsTrail.isEulerian_of_forall_mem

added theorem SimpleGraph.Walk.isEulerian_iff