Theorem List.IsChain.rel_getLast_head_of_append

Modification history

2026-07-02 11:53
Mathlib/Data/List/Chain.lean
feat(Data/List/Chain): generalize `WellFounded.asymmetric₃` to chains (#36922) …
Added List.IsChain.rel_getLast_head_of_appendView on Github →