Theorem List.Lex.nil_left_or_eq_nil

Modification history

2025-03-16 14:08

Mathlib/Data/List/Lex.lean

chore: move `List.Lex` lemmas out of the `List.Lex` namespace (#22935) …

Deleted List.Lex.nil_left_or_eq_nil View on Github →

2023-08-07 08:44

Mathlib/Data/List/Lex.lean

feat: two easy lemmas about List.Lex (#6395) …

Added List.Lex.nil_left_or_eq_nil View on Github →