Theorem List.nextOr_eq_nextOr_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.nextOr_eq_nextOr_of_mem_dropLastView on Github →