Commit 2024-05-16 15:07 95ac1e61

View on Github →

chore: Separate algebraic list lemmas (#12836) Resplit Algebra.BigOperators.List.Basic and Algebra.BigOperators.List.Lemmas into two new files:

  • Algebra.BigOperators.Group.List for lemmas that require group-like structures (Monoid, Group, ...)
  • Algebra.BigOperators.Ring.List for lemmas that require ring-like structures (MonoidWithZero, Ring, ...) Add assert_not_exists Ring in the former. Once https://github.com/leanprover-community/mathlib4/pull/11855 lands, it will be strenghtenable to assert_not_exists MonoidWithZero.

Estimated changes

added theorem List.dvd_prod
deleted theorem List.prod_map_neg
added theorem unop_map_list_prod
deleted theorem Commute.list_sum_left
deleted theorem Commute.list_sum_right
deleted theorem List.dvd_prod
deleted theorem List.dvd_sum
deleted theorem List.prod_eq_zero
deleted theorem List.prod_eq_zero_iff
deleted theorem List.prod_ne_zero
deleted theorem List.sum_map_mul_left
deleted theorem List.sum_map_mul_right
deleted theorem MulOpposite.op_list_prod
deleted theorem unop_map_list_prod
added theorem Commute.list_sum_left
added theorem Commute.list_sum_right
added theorem List.dvd_sum
added theorem List.prod_eq_zero
added theorem List.prod_eq_zero_iff
added theorem List.prod_map_neg
added theorem List.prod_ne_zero
added theorem List.sum_map_mul_left
added theorem List.sum_map_mul_right