Commit 2024-08-19 21:13 b281bae0

View on Github →

feat(Data/List): Some auxiliary lemmas of List (#15536) Add some auxiliary lemmas of List, in preparation of the already finished proof of Bondy-Chvátal theorem.

Estimated changes

Modified Mathlib/Data/List/Lemmas.lean

added theorem List.getElem_reverse'

added theorem List.getElem_tail

added theorem List.getLast_tail

added theorem List.tail_reverse_eq_reverse_dropLast

Modified Mathlib/Data/List/Rotate.lean

added theorem List.IsRotated.cons_getLast_dropLast

added theorem List.IsRotated.dropLast_tail