Theorem List.Lex.singleton_iff

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.singleton_iff View on Github →

2023-08-07 08:44

Mathlib/Data/List/Lex.lean

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

Added List.Lex.singleton_iff View on Github →