mathlib

998ab788 - chore(data/list/lex): make data.list.lex not depend on data.list.basic (#9750)

chore(data/list/lex): make data.list.lex not depend on data.list.basic (#9750) Another simplification in list related dependencies, if this commit breaks external code the fix is to add `import data.list.basic` to the broken file.