Commit 2025-12-01 22:59 16c96d1f

View on Github →

feat(Combinatorics/SimpleGraph): lemmas about the support of cycles (#31758)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean

added theorem SimpleGraph.Walk.mem_support_rotate_iff

Modified Mathlib/Combinatorics/SimpleGraph/Paths.lean

added theorem SimpleGraph.Walk.IsCycle.count_support

added theorem SimpleGraph.Walk.IsCycle.count_support_of_mem