Commit 2023-01-10 12:30 f6f04c93

View on Github →

feat Port/data.list.big operators.lemmas (#1423)

depends on #1380

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/BigOperators/Lemmas.lean

added theorem Commute.list_sum_left

added theorem Commute.list_sum_right

added theorem List.alternatingProd_append

added theorem List.alternatingProd_reverse

added theorem List.dvd_prod

added theorem List.dvd_sum

added theorem List.length_le_sum_of_one_le

added theorem List.neg_one_mem_of_prod_eq_neg_one

added theorem List.pow_card_le_prod

added theorem List.prod_eq_one_iff

added theorem List.sum_map_mul_left

added theorem List.sum_map_mul_right

added theorem MulOpposite.op_list_prod

added theorem MulOpposite.unop_list_prod

added theorem unop_map_list_prod