Commit 2024-04-06 10:45 f9e043cb

chore(Data/List): Do not depend on algebra (#11845) Remove dependencies on algebra in the Data.List folder except for:

• Data.List.EditDistance: Actually relies on algebra. Maybe should be moved?
• Data.List.Card: Completely unused and redundant.
• Data.List.Cycle: Relies on Fintype, which shouldn't rely on algebra but it's hard to fix right now. Maybe should be moved?
• Data.List.Func: Completely unused and redundant.
• Data.List.Lex: That's order theory. Could be moved.
• Data.List.Prime. That's algebra. Should definitely be moved.
• Data.List.Sym: Relies on Multiset, which shouldn't rely on algebra but it's hard to fix right now. Maybe should be moved?
• Data.List.ToFinsupp: That's algebra. Should definitely be moved. As a consequence, move the big operators lemmas that were in there to Algebra.BigOperators.List.Basic. For the lemmas that were Nat-specific and not about auxiliary definitions, keep a version of them in the original file but stated using Nat.sum. Before After