Commit 2024-12-16 10:17 896a59b0

View on Github →

feat(Combinatorics/SimpleGraph): the reverse of a cycle is a cycle (#19611) Added the result that a reverse cycle is a cycle. Includes supporting lemmas concerning lists. In preparation for Tutte's theorem.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Path.lean

added theorem SimpleGraph.Walk.isCycle_reverse

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

added theorem SimpleGraph.Walk.getVert_eq_support_get?

added theorem SimpleGraph.Walk.nodup_tail_support_reverse

Modified Mathlib/Data/List/Basic.lean

added theorem List.drop_length_sub_one

Modified Mathlib/Data/List/Nodup.lean

added theorem List.nodup_tail_reverse