Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-13 23:16 48fd9f25

View on Github →

chore(data/list/big_operators): rename vars, reorder lemmas (#11433)

  • use better variable names;
  • move lemmas to proper sections;
  • relax [comm_semiring R] to [semiring R] in dvd_sum.

Estimated changes

modified theorem list.dvd_prod
modified theorem list.dvd_sum
modified theorem list.eq_of_sum_take_eq
modified theorem list.exists_le_of_sum_le
modified theorem list.exists_lt_of_sum_lt
modified theorem list.length_pos_of_sum_pos
modified theorem list.monotone_sum_take
modified theorem list.nth_zero_mul_tail_prod
modified theorem list.one_le_prod_of_one_le
modified theorem list.one_lt_prod_of_one_lt
modified theorem list.prod_eq_one_iff
modified theorem list.prod_eq_zero
modified theorem list.prod_eq_zero_iff
modified theorem list.prod_erase
modified theorem list.prod_hom
modified theorem list.prod_hom_rel
modified theorem list.prod_hom₂
modified theorem list.prod_inv
modified theorem list.prod_inv_reverse
modified theorem list.prod_is_unit
modified theorem list.prod_join
modified theorem list.prod_map_hom
modified theorem list.prod_ne_zero
modified theorem list.prod_nil
modified theorem list.prod_pos
modified theorem list.prod_reverse_noncomm
modified theorem list.prod_update_nth'
modified theorem list.prod_update_nth
modified theorem list.single_le_prod
modified theorem list.sum_le_foldr_max
modified theorem list.sum_map_mul_left
modified theorem list.sum_map_mul_right
modified theorem monoid_hom.map_list_prod
modified theorem mul_opposite.op_list_prod
modified theorem mul_opposite.unop_list_prod