Theorem List.lt_iff_lex_lt

Modification history

2025-03-05 06:23
Mathlib/Data/List/Lex.lean
feat: generalize order typeclasses (#22569) …
Modified List.lt_iff_lex_ltView on Github →
2025-01-05 03:32
Mathlib/Data/List/Lex.lean
chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464)
Modified List.lt_iff_lex_ltView on Github →
2023-04-12 19:26
Mathlib/Data/List/Lex.lean
chore: move List.lt_iff_lex_lt to a more logical location (#3403)
Modified List.lt_iff_lex_ltView on Github →
2023-04-08 22:11
Mathlib/Data/String/Basic.lean
fix: correct `String.instLinearOrderString` (#3339) …
Added List.lt_iff_lex_ltView on Github →