Commit 2024-04-06 10:45 f9e043cb
View on Github →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 onFintype
, 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 onMultiset
, 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 toAlgebra.BigOperators.List.Basic
. For the lemmas that wereNat
-specific and not about auxiliary definitions, keep a version of them in the original file but stated usingNat.sum
. Before After