# Commit 2024-03-31 00:56 9158f323

View on Github →chore(Data/List): Depend less on big operators (#11741)

- Make
`Data.List.Count`

,`Data.List.Dedup`

,`Data.List.ProdSigma`

,`Data.List.Range`

,`Data.List.Rotate`

,`Data.List.Zip`

not depend on`Data.List.BigOperators.Basic`

. - As a consequence, move the big operators lemmas that were in there to
`Data.List.BigOperators.Basic`

. For the lemmas that were`Nat`

-specific, keep a version of them in the original file but stated using`Nat.sum`

. - To help with this, add
`Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum`

.