Commit 2026-09-15 00:46 11246f19

View on Github →

chore(Combinatorics/SimpleGraph/Trails): golf and cleanup (#41447)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Trails.lean

modified theorem SimpleGraph.Walk.IsEulerian.card_filter_odd_degree

modified theorem SimpleGraph.Walk.IsEulerian.card_odd_degree

modified theorem SimpleGraph.Walk.IsEulerian.edgeSet_eq

modified theorem SimpleGraph.Walk.IsEulerian.edgesFinset_eq

modified theorem SimpleGraph.Walk.IsEulerian.even_degree_iff

modified def SimpleGraph.Walk.IsEulerian.fintypeEdgeSet

modified theorem SimpleGraph.Walk.IsEulerian.isTrail

modified theorem SimpleGraph.Walk.IsEulerian.mem_edges_iff

modified def SimpleGraph.Walk.IsEulerian

modified theorem SimpleGraph.Walk.IsTrail.even_countP_edges_iff

modified theorem SimpleGraph.Walk.IsTrail.isEulerian_iff

modified theorem SimpleGraph.Walk.IsTrail.isEulerian_of_forall_mem

modified theorem SimpleGraph.Walk.isEulerian_iff

Modified Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean

added theorem SimpleGraph.Walk.edgeSet_subset_edgeSet