Commit 2023-04-12 19:26 85a0b4ca

View on Github →

chore: move List.lt_iff_lex_lt to a more logical location (#3403)

Estimated changes

Modified Mathlib/Data/List/Lex.lean

added theorem List.lt_iff_lex_lt

Modified Mathlib/Data/String/Basic.lean

deleted theorem List.lt_iff_lex_lt