Theorem List.next_cons_eq_next_of_mem_dropLast

Modification history

2025-11-29 21:29
Mathlib/Data/List/Cycle.lean
feat(Data/List/Cycle): generalize `next` theorems from `x ∈ l ∧ x ≠ l.getLast` to `x ∈ l.dropLast` (#31958) …
Added List.next_cons_eq_next_of_mem_dropLastView on Github →