Commit 2024-04-05 23:45 f7519d5e

View on Github →

chore(Algebra/BigOperators/List): Use Std lemmas (#11725)

  • Make Algebra.BigOperators.List.Basic, Data.List.Chain not depend on Data.Nat.Order.Basic by using Nat-specific Std lemmas rather than general mathlib ones. I leave the Data.Nat.Basic import since Algebra.BigOperators.List.Basic is algebra territory.
  • Make Algebra.BigOperators.List.Basic not depend on Algebra.Divisibility.Basic. I'm not too sure about that one since they already are algebra. My motivation is that they involve ring-like objects while big operators are about group-like objects, but this is in some sense a second order refactor.
  • As a consequence, move the divisibility and MonoidWithZero lemmas from Algebra.BigOperators.List.Basic to Algebra.BigOperators.List.Lemmas.
  • Move the content of Algebra.BigOperators.List.Defs to Algebra.BigOperators.List.Basic since no file imported the former without the latter and their imports are becoming very close after this PR.
  • Make Data.List.Count, Data.List.Dedup, Data.List.ProdSigma, Data.List.Zip not depend on Algebra.BigOperators.List.Basic.
  • As a consequence, move the big operators lemmas that were in there to Algebra.BigOperators.List.Basic. For the lemmas that were Nat -specific, keep a version of them stated using Nat.sum.
  • To help with this, add Nat.sum_eq_listSum (l : List Nat) : Nat.sum l = l.sum.

Estimated changes

modified theorem List.eq_of_prod_take_eq
added def List.prod
modified theorem List.prod_eq_one
deleted theorem List.prod_eq_zero
deleted theorem List.prod_eq_zero_iff
deleted theorem List.prod_ne_zero
deleted def List.alternatingSum
deleted def List.prod
added theorem List.prod_eq_zero
added theorem List.prod_eq_zero_iff
added theorem List.prod_ne_zero
modified theorem List.Ico.zero_bot
modified theorem Multiset.count_eq_zero
modified theorem Multiset.count_ne_zero