mathlib3

54217b6a - chore(data/list): make separate lexicographic file (#9193)

chore(data/list): make separate lexicographic file (#9193) A minor effort to reduce the `data.list.basic` monolithic, today inspired by yet again being annoyed that I couldn't find something.