Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-18 13:10 2541387e

View on Github →

refactor(data/list/big_operators): review API (#12782)

  • merge prod_monoid into big_operators;
  • review typeclass assumptions in some lemmas;
  • use to_additive in more lemmas.

Estimated changes

deleted theorem list.eq_of_sum_take_eq
deleted theorem list.exists_le_of_sum_le
deleted theorem list.exists_lt_of_sum_lt
deleted theorem list.monotone_sum_take
modified theorem list.one_le_prod_of_one_le
added theorem list.pow_card_le_prod
added theorem list.prod_commute
modified theorem list.prod_eq_one_iff
added theorem list.prod_eq_pow_card
added theorem list.prod_le_pow_card
added theorem list.prod_le_prod'
added theorem list.prod_lt_prod'
added theorem list.prod_repeat
modified theorem list.sum_map_mul_left
modified theorem list.sum_map_mul_right
deleted theorem list.prod_commute
deleted theorem list.prod_eq_pow_card
deleted theorem list.prod_le_pow_card
deleted theorem list.prod_repeat