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

added theorem List.length_sigma
modified theorem List.prod_eq_one
modified theorem List.prod_erase
modified theorem List.prod_erase_of_comm
modified theorem List.prod_map_erase
added theorem List.prod_range_succ'
added theorem List.prod_range_succ
added theorem List.ranges_join
added theorem Nat.sum_eq_listSum
deleted theorem List.countP_join
deleted theorem List.count_bind
deleted theorem List.count_join
deleted theorem List.prod_eq_pow_single
added theorem List.countP_bind
added theorem List.countP_join
added theorem List.count_bind
added theorem List.count_join
added theorem List.length_sigma'
deleted theorem List.length_sigma
deleted theorem List.prod_range_succ'
deleted theorem List.prod_range_succ
added theorem List.ranges_join'
deleted theorem List.ranges_join
modified theorem List.ranges_nodup