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.

Estimated changes