Theorem List.nextOr_eq_nextOr_of_mem_of_ne

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) …
Deleted List.nextOr_eq_nextOr_of_mem_of_neView on Github →
2023-01-27 13:40
Mathlib/Data/List/Cycle.lean
feat: port Data.List.Cycle (#1642)
Added List.nextOr_eq_nextOr_of_mem_of_neView on Github →